src/Pure/General/symbol.ML

   val is_block_ctrl: symbol -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val is_ident: symbol list -> bool
   val beginning: int -> symbol list -> string
-  val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
+  val esc: symbol -> string
+  val escape: string -> string
+  val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a
   val split_words: symbol list -> string list
   val explode_words: string -> string list
-  val esc: symbol -> string
-  val escape: string -> string
   val strip_blanks: string -> string
   val bump_init: string -> string
   val bump_string: string -> string
   val length: symbol list -> int
   val xsymbolsN: string

 val is_block_ctrl = member (op =) ["\\<^bsub>", "\\<^esub>", "\\<^bsup>", "\\<^esup>"];
 
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
 
-fun is_ident [] = false
-  | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
-
 
 
 (** symbol input **)
 
-(* scanning through symbols *)
+(* source *)
+
+local
+
+fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\";
+
+fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
+
+fun implode_pseudo_utf8 (cs as ["\192", c]) =
+      if ord c < 160 then chr (ord c - 128) else implode cs
+  | implode_pseudo_utf8 cs = implode cs;
+
+val scan_encoded_newline =
+  $$ "\^M" -- $$ "\n" >> K "\n" ||
+  $$ "\^M" >> K "\n" ||
+  Scan.this_string "\\<^newline>" >> K "\n";
+
+val scan_raw =
+  Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
+  Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
+
+val scan_total =
+  Scan.one is_plain ||
+  Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
+  scan_encoded_newline ||
+  ($$ "\\" ^^ $$ "<" ^^
+    (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^
+      Scan.optional ($$ ">") "")) ||
+  Scan.one not_eof;
+
+in
+
+fun source src = Source.source stopper (Scan.bulk scan_total) NONE src;
+
+end;
+
+
+(* explode *)
+
+local
+
+fun no_explode [] = true
+  | no_explode ("\\" :: "<" :: _) = false
+  | no_explode ("\^M" :: _) = false
+  | no_explode (c :: cs) = is_ascii c andalso no_explode cs;
+
+in
+
+fun sym_explode str =
+  let val chs = raw_explode str in
+    if no_explode chs then chs
+    else Source.exhaust (source (Source.of_list chs))
+  end;
+
+end;
+
+
+(* escape *)
+
+val esc = fn s =>
+  if is_char s then s
+  else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
+  else "\\" ^ s;
+
+val escape = implode o map esc o sym_explode;
+
+
+
+(** scanning through symbols **)
+
+(* scanner *)
 
 fun scanner msg scan syms =
   let
     fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
       | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss));

       (result, []) => result
     | (_, rest) => error (message (rest, NONE) ()))
   end;
 
 
-(* source *)
-
-local
-
-fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\";
-
-fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
-
-fun implode_pseudo_utf8 (cs as ["\192", c]) =
-      if ord c < 160 then chr (ord c - 128) else implode cs
-  | implode_pseudo_utf8 cs = implode cs;
-
-val scan_encoded_newline =
-  $$ "\^M" -- $$ "\n" >> K "\n" ||
-  $$ "\^M" >> K "\n" ||
-  Scan.this_string "\\<^newline>" >> K "\n";
-
-val scan_raw =
-  Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
-  Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode);
-
-val scan_total =
-  Scan.one is_plain ||
-  Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
-  scan_encoded_newline ||
-  ($$ "\\" ^^ $$ "<" ^^
-    (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^
-      Scan.optional ($$ ">") "")) ||
-  Scan.one not_eof;
-
-in
-
-fun source src = Source.source stopper (Scan.bulk scan_total) NONE src;
-
-end;
-
-
-(* explode *)
-
-local
-
-fun no_explode [] = true
-  | no_explode ("\\" :: "<" :: _) = false
-  | no_explode ("\^M" :: _) = false
-  | no_explode (c :: cs) = is_ascii c andalso no_explode cs;
-
-in
-
-fun sym_explode str =
-  let val chs = raw_explode str in
-    if no_explode chs then chs
-    else Source.exhaust (source (Source.of_list chs))
-  end;
-
-end;
-
-
 (* space-separated words *)
 
 val scan_word =
   Scan.many1 is_ascii_blank >> K NONE ||
   Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);
 
 val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
 
 val explode_words = split_words o sym_explode;
-
-
-(* escape *)
-
-val esc = fn s =>
-  if is_char s then s
-  else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s
-  else "\\" ^ s;
-
-val escape = implode o map esc o sym_explode;
 
 
 (* blanks *)
 
 fun strip_blanks s =
   sym_explode s
   |> take_prefix is_blank |> #2
   |> take_suffix is_blank |> #1
   |> implode;
+
+
+(* identifiers *)
+
+fun is_ident [] = false
+  | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
 
 
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\\<^isub>" :: _) = true