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  

     2.1 --- a/src/Pure/Thy/latex.ML	Sat Apr 01 20:26:20 2000 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Mon Apr 03 14:00:16 2000 +0200
     2.3 @@ -7,7 +7,8 @@
     2.4  
     2.5  signature LATEX =
     2.6  sig
     2.7 -  datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
     2.8 +  datatype token = Basic of OuterLex.token | Markup of string * string |
     2.9 +    MarkupEnv of string * string | Verbatim of string
    2.10    val old_symbol_source: string -> Symbol.symbol list -> string
    2.11    val token_source: token list -> string
    2.12    val theory_entry: string -> string
    2.13 @@ -57,7 +58,11 @@
    2.14  
    2.15  structure T = OuterLex;
    2.16  
    2.17 -datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
    2.18 +datatype token =
    2.19 +  Basic of T.token |
    2.20 +  Markup of string * string |
    2.21 +  MarkupEnv of string * string |
    2.22 +  Verbatim of string;
    2.23  
    2.24  
    2.25  val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    2.26 @@ -80,6 +85,8 @@
    2.27          else output_syms s
    2.28        end
    2.29    | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    2.30 +  | output_tok (MarkupEnv (cmd, txt)) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    2.31 +      strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    2.32    | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
    2.33  
    2.34  

     3.1 --- a/src/Pure/Thy/present.ML	Sat Apr 01 20:26:20 2000 +0200
     3.2 +++ b/src/Pure/Thy/present.ML	Mon Apr 03 14:00:16 2000 +0200
     3.3 @@ -20,6 +20,7 @@
     3.4    type token
     3.5    val basic_token: OuterLex.token -> token
     3.6    val markup_token: string * string -> token
     3.7 +  val markup_env_token: string * string -> token
     3.8    val verbatim_token: string -> token
     3.9    val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
    3.10    val token_source: string -> (unit -> token list) -> unit
    3.11 @@ -375,6 +376,7 @@
    3.12  type token = Latex.token;
    3.13  val basic_token = Latex.Basic;
    3.14  val markup_token = Latex.Markup;
    3.15 +val markup_env_token = Latex.MarkupEnv;
    3.16  val verbatim_token = Latex.Verbatim;
    3.17  
    3.18  fun old_symbol_source name mk_text =