+
Point of view
All features
class JSON_STRING
Summary
top
Direct parents
Inherit list: JSON_VALUE
Insert list: HASHABLE, UNICODE_STRING_HELPER
Class invariant
top
Overview
top
Creation features
{JSON_HANDLER}
Features
{ANY}
{JSON_HANDLER}
{}
{ANY}
{JSON_HANDLER}
{ANY}
accept (visitor: VISITOR)
effective procedure
{ANY}
top
Accept to be visited by the visitor.
require
  • visitor /= Void
hash_code: INTEGER_32
writable attribute
{ANY}
top
The hash-code value of Current.
ensure
  • good_hash_value: Result >= 0
is_equal (other: JSON_STRING): BOOLEAN
effective function
{ANY}
top
Is other attached to an object considered equal to current object?
require
    • other /= Void
    • other /= Void
ensure
  • Result implies hash_code = other.hash_code
  • commutative: generating_type = other.generating_type implies Result = other.is_equal(Current)
append_in (str: STRING, raw: BOOLEAN)
effective procedure
{ANY}
top
Append the JSON string into str If raw is True, append raw UTF-8 codes; otherwise, use '\u' sequences
require
  • str /= Void
write_to (str: OUTPUT_STREAM, raw: BOOLEAN)
effective procedure
{ANY}
top
Write the JSON string to str If raw is True, write raw UTF-8 codes; otherwise, use '\u' sequences
require
  • str.is_connected
out_in_tagged_out_memory
effective procedure
{ANY}
top
Append terse printable representation of current object in tagged_out_memory.
require
    • locked: tagged_out_locked
    • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
  • not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
  • append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))
writable attribute
{JSON_HANDLER}
top
invalidate
effective procedure
{JSON_HANDLER}
top
Allows to modify the string, e.g.
to clean it. Note: an invalidated string cannot be revalidated.
is_valid: BOOLEAN
writable attribute
{JSON_HANDLER}
top
make (a_string: UNICODE_STRING)
effective procedure
{}
top
require
  • a_string /= Void
ensure
from_string (a_string: ABSTRACT_STRING)
effective procedure
{}
top
append_unicode_in (str: OUTPUT_STREAM, u: INTEGER_32)
effective procedure
{}
top
set_string_invariant (a_string: UNICODE_STRING): BOOLEAN
effective function
{}
top
require
  • a_string /= Void
string_invariant: UNICODE_STRING
writable attribute
{}
top
line: INTEGER_32
writable attribute
{ANY}
top
optional line and column; 0 if not set
column: INTEGER_32
writable attribute
{ANY}
top
optional line and column; 0 if not set
set_position (a_line: INTEGER_32, a_column: INTEGER_32)
effective procedure
{JSON_HANDLER}
top
ensure
utf8_character_in (character: INTEGER_32, s: STRING)
effective procedure
{ANY}
top
require
  • character >= 0
  • s /= Void