src/Pure/General/symbol.ML
author schirmer
Mon Jan 26 10:34:02 2004 +0100 (2004-01-26)
changeset 14361 ad2f5da643b4
parent 14234 9590df3c5f2a
child 14557 31ae4a47267c
permissions -rw-r--r--
* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy
     1 (*  Title:      Pure/General/symbol.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Generalized characters with infinitely many named symbols.
     7 *)
     8 
     9 signature SYMBOL =
    10 sig
    11   type symbol
    12   val space: symbol
    13   val spaces: int -> symbol
    14   val sync: symbol
    15   val is_sync: symbol -> bool
    16   val not_sync: symbol -> bool
    17   val malformed: symbol
    18   val eof: symbol
    19   val is_eof: symbol -> bool
    20   val not_eof: symbol -> bool
    21   val stopper: symbol * (symbol -> bool)
    22   val is_ascii: symbol -> bool
    23   val is_letter: symbol -> bool
    24   val is_digit: symbol -> bool
    25   val is_quasi: symbol -> bool
    26   val is_quasi_letter: symbol -> bool
    27   val is_letdig: symbol -> bool
    28   val is_blank: symbol -> bool
    29   val is_identifier: symbol -> bool
    30   val is_symbolic: symbol -> bool
    31   val is_printable: symbol -> bool
    32   val length: symbol list -> int
    33   val strip_blanks: string -> string
    34   val beginning: symbol list -> string
    35   val scan_id: string list -> string * string list
    36   val scan: string list -> symbol * string list
    37   val scanner: string -> (symbol list -> 'a * symbol list) -> symbol list -> 'a
    38   val source: bool -> (string, 'a) Source.source ->
    39     (symbol, (string, 'a) Source.source) Source.source
    40   val explode: string -> symbol list
    41   val bump_string: string -> string
    42   val default_indent: string * int -> string
    43   val add_mode: string -> (string -> string * real) * (string * int -> string) -> unit
    44   val symbolsN: string
    45   val xsymbolsN: string
    46   val plain_output: string -> string
    47   val output: string -> string
    48   val output_width: string -> string * real
    49   val indent: string * int -> string
    50 end;
    51 
    52 structure Symbol: SYMBOL =
    53 struct
    54 
    55 
    56 (** generalized characters **)
    57 
    58 (*symbols, which are considered the smallest entities of any Isabelle
    59   string, may be of the following form:
    60     (a) ASCII symbols: a
    61     (b) printable symbols: \<ident>
    62     (c) control symbols: \<^ctrlident>
    63 
    64   output is subject to the print_mode variable (default: verbatim),
    65   actual interpretation in display is up to front-end tools;
    66 *)
    67 
    68 type symbol = string;
    69 
    70 val space = " ";
    71 fun spaces k = Library.replicate_string k space;
    72 val sync = "\\<^sync>";
    73 val malformed = "\\<^malformed>";
    74 val eof = "";
    75 
    76 
    77 (* kinds *)
    78 
    79 fun is_sync s = s = sync;
    80 fun not_sync s = s <> sync;
    81 
    82 fun is_eof s = s = eof;
    83 fun not_eof s = s <> eof;
    84 val stopper = (eof, is_eof);
    85 
    86 fun is_ascii s = size s = 1 andalso ord s < 128;
    87 
    88 local
    89     fun wrap s = "\\<" ^ s ^ ">"
    90 
    91     val cal_letters =
    92 	["A","B","C","D","E","F","G","H","I","J","K","L","M",
    93 	 "N","O","P","Q","R","S","T","U","V","W","X","Y","Z"]
    94 
    95     val small_letters =
    96 	["a","b","c","d","e","f","g","h","i","j","k","l","m",
    97 	 "n","o","p","q","r","s","t","u","v","w","x","y","z"]
    98 
    99     val goth_letters =
   100 	["AA","BB","CC","DD","EE","FF","GG","HH","II","JJ","KK","LL","MM",
   101 	 "NN","OO","PP","QQ","RR","SS","TT","UU","VV","WW","XX","YY","ZZ",
   102 	 "aa","bb","cc","dd","ee","ff","gg","hh","ii","jj","kk","ll","mm",
   103 	 "nn","oo","pp","qq","rr","ss","tt","uu","vv","ww","xx","yy","zz"]
   104 
   105     val greek_letters =
   106 	["alpha","beta","gamma","delta","epsilon","zeta","eta","theta",
   107 	 "iota","kappa",(*"lambda",*)"mu","nu","xi","pi","rho","sigma","tau",
   108 	 "upsilon","phi","psi","omega","Gamma","Delta","Theta","Lambda",
   109 	 "Xi","Pi","Sigma","Upsilon","Phi","Psi","Omega"]
   110 
   111     val bbb_letters = ["bool","complex","nat","rat","real","int"]
   112 
   113     val control_letters = ["^isub", "^isup"]
   114  
   115     val pre_letters =
   116 	cal_letters   @
   117 	small_letters @
   118 	goth_letters  @
   119 	greek_letters @
   120 	control_letters
   121 
   122 in
   123 val ext_letters = map wrap pre_letters 
   124 
   125 fun is_ext_letter s = String.isPrefix "\\<" s andalso s mem ext_letters
   126 end
   127      
   128 fun is_letter s =
   129     (size s = 1 andalso
   130      (ord "A" <= ord s andalso ord s <= ord "Z" orelse
   131       ord "a" <= ord s andalso ord s <= ord "z"))
   132     orelse is_ext_letter s
   133 
   134 fun is_digit s =
   135     size s = 1 andalso ord "0" <= ord s andalso ord s <= ord "9"
   136 
   137 fun is_quasi "_" = true
   138   | is_quasi "'" = true
   139   | is_quasi _ = false;
   140 
   141 fun is_quasi_letter s = is_quasi s orelse is_letter s;
   142 
   143 val is_blank =
   144   fn " " => true | "\t" => true | "\r" => true | "\n" => true | "\^L" => true
   145     | "\160" => true | "\\<spacespace>" => true
   146     | _ => false;
   147 
   148 fun is_letdig s = is_quasi_letter s orelse is_digit s;
   149 
   150 fun is_symbolic s =
   151   size s > 2 andalso nth_elem_string (2, s) <> "^"
   152   andalso not (is_ext_letter s);
   153 
   154 fun is_printable s =
   155   size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
   156   is_ext_letter s orelse
   157   is_symbolic s;
   158 
   159 fun is_ctrl_letter s =
   160   size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" andalso s <> ">";
   161 
   162 fun is_identifier s =
   163   case (explode s) of
   164       [] => false
   165     | c::cs => is_letter c andalso forall is_letdig cs;
   166 
   167 fun sym_length ss = foldl (fn (n, s) =>
   168   (if not (is_printable s) then 0 else
   169     (case Library.try String.substring (s, 2, 4) of
   170       Some s' => if s' = "long" orelse s' = "Long" then 2 else 1
   171     | None => 1)) + n) (0, ss);
   172 
   173 fun strip_blanks s =
   174   implode (#1 (Library.take_suffix is_blank (#2 (Library.take_prefix is_blank (explode s)))));
   175 
   176 
   177 (* beginning *)
   178 
   179 val smash_blanks = map (fn s => if is_blank s then space else s);
   180 
   181 fun beginning raw_ss =
   182   let
   183     val (all_ss, _) = take_suffix is_blank raw_ss;
   184     val dots = if length all_ss > 10 then " ..." else "";
   185     val (ss, _) = take_suffix is_blank (take (10, all_ss));
   186   in implode (smash_blanks ss) ^ dots end;
   187 
   188 
   189 
   190 (** scanning through symbols **)
   191 
   192 fun scanner msg scan chs =
   193   let
   194     fun err_msg cs = msg ^ ": " ^ beginning cs;
   195     val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan));
   196   in
   197     (case fin_scan chs of
   198       (result, []) => result
   199     | (_, rest) => error (err_msg rest))
   200   end;
   201 
   202 
   203 
   204 (** symbol input **)
   205 
   206 (* scan *)
   207 
   208 val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
   209 val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode);
   210 
   211 val scan =
   212   $$ "\\" ^^ $$ "<" ^^
   213     !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
   214        ((($$ "^" ^^ scan_ctrlid) || scan_id) ^^ $$ ">") ||
   215   Scan.one not_eof;
   216 
   217 (* source *)
   218 
   219 val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed];
   220 
   221 fun source do_recover src =
   222   Source.source stopper (Scan.bulk scan) (if do_recover then Some recover else None) src;
   223 
   224 
   225 (* explode *)
   226 
   227 fun no_syms [] = true
   228   | no_syms ("\\" :: "<" :: _) = false
   229   | no_syms (_ :: cs) = no_syms cs;
   230 
   231 fun sym_explode str =
   232   let val chs = explode str in
   233     if no_syms chs then chs     (*tune trivial case*)
   234     else the (Scan.read stopper (Scan.repeat scan) chs)
   235   end;
   236 
   237 
   238 (* bump_string -- increment suffix of lowercase letters like a base 26 number *)
   239 
   240 fun bump_string str =
   241   let
   242     fun bump [] = ["a"]
   243       | bump ("z" :: ss) = "a" :: bump ss
   244       | bump (s :: ss) =
   245           if size s = 1 andalso ord "a" <= ord s andalso ord s < ord "z"
   246           then chr (ord s + 1) :: ss
   247           else "a" :: s :: ss;
   248     val (cs, qs) = Library.take_suffix is_quasi (sym_explode str);
   249   in implode (rev (bump (rev cs)) @ qs) end;
   250 
   251 
   252 (** symbol output **)
   253 
   254 (* default *)
   255 
   256 fun string_size s = (s, real (size s));
   257 
   258 val escape = Scan.repeat
   259   ((($$ "\\" >> K "\\\\") ^^ Scan.optional ($$ "\\" >> K "\\\\") "" ^^ $$ "<" ^^
   260       Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
   261    Scan.one not_eof) >> implode;
   262 
   263 fun default_output s =
   264   if not (exists_string (equal "\\") s) then string_size s
   265   else string_size (fst (Scan.finite stopper escape (explode s)));
   266 
   267 fun default_indent (_: string, k) = spaces k;
   268 
   269 
   270 (* maintain modes *)
   271 
   272 val symbolsN = "symbols";
   273 val xsymbolsN = "xsymbols";
   274 
   275 val modes =
   276   ref (Symtab.empty: ((string -> string * real) * (string * int -> string)) Symtab.table);
   277 
   278 fun lookup_mode name = Symtab.lookup (! modes, name);
   279 
   280 fun add_mode name m =
   281  (if is_none (lookup_mode name) then ()
   282   else warning ("Redeclaration of symbol print mode " ^ quote name);
   283   modes := Symtab.update ((name, m), ! modes));
   284 
   285 fun get_mode () =
   286   if_none (get_first lookup_mode (! print_mode)) (default_output, default_indent);
   287 
   288 
   289 (* mode output *)
   290 
   291 fun output_width x = #1 (get_mode ()) x;
   292 val output = #1 o output_width;
   293 val plain_output = #1 o default_output;
   294 
   295 fun indent x = #2 (get_mode ()) x;
   296 
   297 
   298 (*final declarations of this structure!*)
   299 val length = sym_length;
   300 val explode = sym_explode;
   301 
   302 
   303 end;