1.1 --- a/NEWS	Wed Apr 14 11:44:57 2004 +0200
     1.2 +++ b/NEWS	Wed Apr 14 12:19:16 2004 +0200
     1.3 @@ -32,13 +32,10 @@
     1.4    PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
     1.5    new control characters are not identifier parts.
     1.6  
     1.7 -* Pure: Control-symbols of the form \<^raw...> will literally print the
     1.8 +* Pure: Control-symbols of the form \<^raw:...> will literally print the
     1.9    content of ... to the latex file instead of \isacntrl... . The ... 
    1.10    accepts all printable characters excluding the end bracket >.
    1.11  
    1.12 -* Pure: Symbols may only start with one backslash: \<...>. \\<...> is no 
    1.13 -  longer accepted by the scanner.
    1.14 -
    1.15  * Pure: Using new Isar command "finalconsts" (or the ML functions
    1.16    Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.17    declare constants "final", which prevents their being given a definition

     2.1 --- a/src/Pure/General/symbol.ML	Wed Apr 14 11:44:57 2004 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Wed Apr 14 12:19:16 2004 +0200
     2.3 @@ -37,6 +37,7 @@
     2.4    val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
     2.5    val source: bool -> (string, 'a) Source.source ->
     2.6      (symbol, (string, 'a) Source.source) Source.source
     2.7 +  val escape: string -> string
     2.8    val explode: string -> symbol list
     2.9    val bump_string: string -> string
    2.10    val default_indent: string * int -> string
    2.11 @@ -60,11 +61,17 @@
    2.12      (a) ASCII symbols: a
    2.13      (b) printable symbols: \<ident>
    2.14      (c) control symbols: \<^ident>
    2.15 -    (d) raw control symbols: \<^raw...>, where "..." may be any printable
    2.16 +    (d) raw control symbols: \<^raw:...>, where "..." may be any printable
    2.17          character excluding ">"
    2.18  
    2.19    output is subject to the print_mode variable (default: verbatim),
    2.20    actual interpretation in display is up to front-end tools;
    2.21 +
    2.22 +  Symbols (b),(c) and (d) may optionally start with "\\" instead of just "\" 
    2.23 +  for compatibility with ML-strings of old style theory and ML-files and 
    2.24 +  isa-ProofGeneral. The default output of these symbols will also start with "\\".
    2.25 +  This is used by the Isar ML-command to convert Isabelle-strings to ML-strings, 
    2.26 +  before evaluation.
    2.27  *)
    2.28  
    2.29  type symbol = string;
    2.30 @@ -209,10 +216,11 @@
    2.31  
    2.32  val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
    2.33  val scan_rawctrlid = 
    2.34 -    $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ (Scan.any is_ctrl_letter >> implode);
    2.35 +    $$ "r" ^^ $$ "a" ^^ $$ "w" ^^ $$ ":" ^^ (Scan.any is_ctrl_letter >> implode);
    2.36 +
    2.37  
    2.38  val scan =
    2.39 -  $$ "\\" ^^ $$ "<" ^^
    2.40 +  ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
    2.41      !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
    2.42         ((($$ "^" ^^ (scan_rawctrlid || scan_id)) || scan_id) ^^ $$ ">") ||
    2.43    Scan.one not_eof;
    2.44 @@ -258,13 +266,11 @@
    2.45  
    2.46  fun string_size s = (s, real (size s));
    2.47  
    2.48 -val escape = Scan.repeat
    2.49 -  ((($$ "\\" >> K "\\\\") ^^ Scan.optional ($$ "\\" >> K "\\\\") "" ^^ $$ "<" ^^
    2.50 -      Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
    2.51 -   Scan.one not_eof) >> implode;
    2.52 +fun sym_escape s = if size s = 1 then s else "\\" ^ s;
    2.53  
    2.54 -
    2.55 -val default_output = string_size
    2.56 +fun default_output s =
    2.57 +  if not (exists_string (equal "\\") s) then string_size s
    2.58 +  else string_size (implode (map sym_escape (sym_explode s)));
    2.59  
    2.60  fun default_indent (_: string, k) = spaces k;
    2.61  
    2.62 @@ -292,16 +298,14 @@
    2.63  
    2.64  fun output_width x = #1 (get_mode ()) x;
    2.65  val output = #1 o output_width;
    2.66 -fun plain_output s =   
    2.67 -  if not (exists_string (equal "\\") s) then s
    2.68 -  else fst (Scan.finite stopper escape (explode s));
    2.69 -
    2.70 +val plain_output = #1 o default_output;
    2.71 +  
    2.72  fun indent x = #2 (get_mode ()) x;
    2.73  
    2.74  
    2.75  (*final declarations of this structure!*)
    2.76  val length = sym_length;
    2.77  val explode = sym_explode;
    2.78 -
    2.79 +val escape = sym_escape;
    2.80  
    2.81  end;

     3.1 --- a/src/Pure/Thy/latex.ML	Wed Apr 14 11:44:57 2004 +0200
     3.2 +++ b/src/Pure/Thy/latex.ML	Wed Apr 14 12:19:16 2004 +0200
     3.3 @@ -69,7 +69,7 @@
     3.4    if size s = 1 then output_chr s
     3.5    else
     3.6      (case explode s of
     3.7 -      "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) 
     3.8 +      "\\" :: "<" :: "^" :: "r"::"a"::"w"::":"::cs => implode (#1 (Library.split_last cs)) 
     3.9      | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
    3.10      | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    3.11      | _ => sys_error "output_sym");

     4.1 --- a/src/Pure/proof_general.ML	Wed Apr 14 11:44:57 2004 +0200
     4.2 +++ b/src/Pure/proof_general.ML	Wed Apr 14 12:19:16 2004 +0200
     4.3 @@ -48,7 +48,7 @@
     4.4  fun xsymbols_output s =
     4.5    if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
     4.6      let val syms = Symbol.explode s
     4.7 -    in (s, real (Symbol.length syms)) end
     4.8 +    in (implode (map Symbol.escape syms), real (Symbol.length syms)) end
     4.9    else (s, real (size s));
    4.10  
    4.11  fun pgml_output (s, len) =