isabelle update -u control_cartouches;

more explicit notion of ord value for HOL characters

typo

--HG--
extra : rebase_source : 8da435e75768a6ddec58e33a5abcb5af447cda42

proper datatype for 8-bit characters

model characters directly as range 0..255
* * *
operate on syntax terms rather than asts

modernized setup;

inner syntax token language allows regular quoted strings;
tuned signature;

added \<newline> symbol, which is used for char/string literals in HOL;

syntax translations always depend on context;

systematic conversions between nat and nibble/char;
more uniform approaches to execute operations on nibble/char

--HG--
extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d

renamed "xstr" to "str_token";

inner syntax positions for string literals;

discontinued special treatment of structure Lexicon;

discontinued old-style Syntax.constrainC;

discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

explicit @{type_syntax} markup;

slightly more abstract syntax mark/unmark operations;

adapted to authentic syntax;

modernized structures;

modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;

refined HOL string theories and corresponding ML fragments

renamed token markup "_xstr" to "_inner_string";

proper Sign operations instead of Theory aliases;

specials: include single quote;

Concrete syntax for hex chars and strings.

removed;

Tools/string_syntax.ML;