src/Pure/General/symbol.ML
changeset 14361 ad2f5da643b4
parent 14234 9590df3c5f2a
child 14557 31ae4a47267c
     1.1 --- a/src/Pure/General/symbol.ML	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/src/Pure/General/symbol.ML	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4    string, may be of the following form:
     1.5      (a) ASCII symbols: a
     1.6      (b) printable symbols: \<ident>
     1.7 -    (c) control symbols: \<^ident>
     1.8 +    (c) control symbols: \<^ctrlident>
     1.9  
    1.10    output is subject to the print_mode variable (default: verbatim),
    1.11    actual interpretation in display is up to front-end tools;
    1.12 @@ -156,6 +156,9 @@
    1.13    is_ext_letter s orelse
    1.14    is_symbolic s;
    1.15  
    1.16 +fun is_ctrl_letter s =
    1.17 +  size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" andalso s <> ">";
    1.18 +
    1.19  fun is_identifier s =
    1.20    case (explode s) of
    1.21        [] => false
    1.22 @@ -203,14 +206,14 @@
    1.23  (* scan *)
    1.24  
    1.25  val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
    1.26 +val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode);
    1.27  
    1.28  val scan =
    1.29 -  ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
    1.30 +  $$ "\\" ^^ $$ "<" ^^
    1.31      !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
    1.32 -      (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
    1.33 +       ((($$ "^" ^^ scan_ctrlid) || scan_id) ^^ $$ ">") ||
    1.34    Scan.one not_eof;
    1.35  
    1.36 -
    1.37  (* source *)
    1.38  
    1.39  val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed];