src/Pure/Isar/outer_syntax.ML
changeset 7789 57d20133224e
parent 7774 6da9b544a12d
child 7810 e5f15a673a69
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 17:20:19 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 17:20:58 1999 +0200
     1.3 @@ -44,6 +44,8 @@
     1.4      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.5    val markup_command: string -> string -> string ->
     1.6      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.7 +  val verbatim_command: string -> string -> string ->
     1.8 +    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.9    val improper_command: string -> string -> string ->
    1.10      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.11    val dest_keywords: unit -> string list
    1.12 @@ -100,7 +102,7 @@
    1.13  type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    1.14  
    1.15  datatype parser =
    1.16 -  Parser of string * (string * string * bool) * bool * parser_fn;
    1.17 +  Parser of string * (string * string * bool option) * bool * parser_fn;
    1.18  
    1.19  fun parser int_only markup name comment kind parse =
    1.20    Parser (name, (comment, kind, markup), int_only, parse);
    1.21 @@ -138,8 +140,8 @@
    1.22  
    1.23  val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
    1.24  val global_parsers =
    1.25 -  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool) Symtab.table);
    1.26 -val global_markups = ref ([]: string list);
    1.27 +  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool option) Symtab.table);
    1.28 +val global_markups = ref ([]: (string * bool) list);
    1.29  
    1.30  fun change_lexicons f =
    1.31    let val lexs = f (! global_lexicons) in
    1.32 @@ -148,8 +150,8 @@
    1.33      | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
    1.34    end;
    1.35  
    1.36 -fun get_markup (names, (name, (_, true))) = name :: names
    1.37 -  | get_markup (names, _) = names;
    1.38 +fun get_markup (ms, (name, (_, Some m))) = (name, m) :: ms
    1.39 +  | get_markup (ms, _) = ms;
    1.40  
    1.41  fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
    1.42  fun change_parsers f = (global_parsers := f (! global_parsers); make_markups ());
    1.43 @@ -165,7 +167,10 @@
    1.44  fun get_lexicons () = ! global_lexicons;
    1.45  fun get_parsers () = ! global_parsers;
    1.46  fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
    1.47 -fun is_markup name = name mem_string ! global_markups;
    1.48 +
    1.49 +fun lookup_markup name = assoc (! global_markups, name);
    1.50 +fun is_markup name = if_none (lookup_markup name) false;
    1.51 +fun is_verbatim name = if_none (apsome not (lookup_markup name)) false;
    1.52  
    1.53  
    1.54  (* augment syntax *)
    1.55 @@ -335,11 +340,14 @@
    1.56  
    1.57  val improper = Scan.any (not o T.is_proper);
    1.58  val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    1.59 +val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
    1.60  
    1.61  val present_token =
    1.62    improper |-- markup -- (improper |-- P.text --| (improper -- Scan.option semicolon -- improper))
    1.63      >> Present.markup_token ||
    1.64    (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
    1.65 +  (improper -- verbatim -- improper) |-- P.text --| (improper -- Scan.option semicolon -- improper)
    1.66 +    >> Present.verbatim_token ||
    1.67    Scan.one T.not_eof >> Present.basic_token;
    1.68  
    1.69  in
    1.70 @@ -446,9 +454,10 @@
    1.71  
    1.72  
    1.73  (*final declarations of this structure!*)
    1.74 -val command = parser false false;
    1.75 -val markup_command = parser false true;
    1.76 -val improper_command = parser true false;
    1.77 +val command = parser false None;
    1.78 +val markup_command = parser false (Some true);
    1.79 +val verbatim_command = parser false (Some false);
    1.80 +val improper_command = parser true None;
    1.81  
    1.82  
    1.83  end;