src/Pure/Isar/outer_syntax.ML
changeset 8660 e5048a26e1d8
parent 8652 39a695b0b1d7
child 8720 840c75ab2a7f
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 01 20:26:20 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 03 14:00:16 2000 +0200
     1.3 @@ -45,6 +45,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 markup_env_command: string -> string -> string ->
     1.8 +    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.9    val verbatim_command: string -> string -> string ->
    1.10      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.11    val improper_command: string -> string -> string ->
    1.12 @@ -104,8 +106,10 @@
    1.13  type token = T.token;
    1.14  type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    1.15  
    1.16 +datatype markup_kind = Markup | MarkupEnv | Verbatim;
    1.17 +
    1.18  datatype parser =
    1.19 -  Parser of string * (string * string * bool option) * bool * parser_fn;
    1.20 +  Parser of string * (string * string * markup_kind option) * bool * parser_fn;
    1.21  
    1.22  fun parser int_only markup name comment kind parse =
    1.23    Parser (name, (comment, kind, markup), int_only, parse);
    1.24 @@ -143,8 +147,8 @@
    1.25  
    1.26  val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
    1.27  val global_parsers =
    1.28 -  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool option) Symtab.table);
    1.29 -val global_markups = ref ([]: (string * bool) list);
    1.30 +  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * markup_kind option) Symtab.table);
    1.31 +val global_markups = ref ([]: (string * markup_kind) list);
    1.32  
    1.33  fun change_lexicons f =
    1.34    let val lexs = f (! global_lexicons) in
    1.35 @@ -172,8 +176,7 @@
    1.36  fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
    1.37  
    1.38  fun lookup_markup name = assoc (! global_markups, name);
    1.39 -fun is_markup name = if_none (lookup_markup name) false;
    1.40 -fun is_verbatim name = if_none (apsome not (lookup_markup name)) false;
    1.41 +fun is_markup kind name = (case lookup_markup name of Some k => k = kind | None => false);
    1.42  
    1.43  
    1.44  (* augment syntax *)
    1.45 @@ -365,12 +368,16 @@
    1.46    opt_newline -- Scan.one T.is_begin_ignore --
    1.47      P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore -- opt_newline);
    1.48  
    1.49 -val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    1.50 -val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
    1.51 +fun markup_kind k = Scan.one (T.is_kind T.Command andf is_markup k o T.val_of);
    1.52 +
    1.53 +val markup = markup_kind Markup >> T.val_of;
    1.54 +val markup_env = markup_kind MarkupEnv >> T.val_of;
    1.55 +val verbatim = markup_kind Verbatim;
    1.56  
    1.57  val present_token =
    1.58    ignore_stuff >> K None ||
    1.59    (improper |-- markup -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_token ||
    1.60 +    improper |-- markup_env -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_env_token ||
    1.61      (P.$$$ "--" >> K "cmt") -- P.!!!! (improper |-- P.text) >> Present.markup_token ||
    1.62      (improper -- verbatim) |-- P.!!!! (improper |-- P.text --| improper_end)
    1.63        >> Present.verbatim_token ||
    1.64 @@ -482,8 +489,9 @@
    1.65  
    1.66  (*final declarations of this structure!*)
    1.67  val command = parser false None;
    1.68 -val markup_command = parser false (Some true);
    1.69 -val verbatim_command = parser false (Some false);
    1.70 +val markup_command = parser false (Some Markup);
    1.71 +val markup_env_command = parser false (Some MarkupEnv);
    1.72 +val verbatim_command = parser false (Some Verbatim);
    1.73  val improper_command = parser true None;
    1.74  
    1.75