support markup environments;

--- a/src/Pure/Isar/outer_syntax.ML	Sat Apr 01 20:26:20 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 03 14:00:16 2000 +0200
@@ -45,6 +45,8 @@
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val markup_command: string -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
+  val markup_env_command: string -> string -> string ->
+    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val verbatim_command: string -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val improper_command: string -> string -> string ->
@@ -104,8 +106,10 @@
 type token = T.token;
 type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
 
+datatype markup_kind = Markup | MarkupEnv | Verbatim;
+
 datatype parser =
-  Parser of string * (string * string * bool option) * bool * parser_fn;
+  Parser of string * (string * string * markup_kind option) * bool * parser_fn;
 
 fun parser int_only markup name comment kind parse =
   Parser (name, (comment, kind, markup), int_only, parse);
@@ -143,8 +147,8 @@
 
 val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
 val global_parsers =
-  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool option) Symtab.table);
-val global_markups = ref ([]: (string * bool) list);
+  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * markup_kind option) Symtab.table);
+val global_markups = ref ([]: (string * markup_kind) list);
 
 fun change_lexicons f =
   let val lexs = f (! global_lexicons) in
@@ -172,8 +176,7 @@
 fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
 
 fun lookup_markup name = assoc (! global_markups, name);
-fun is_markup name = if_none (lookup_markup name) false;
-fun is_verbatim name = if_none (apsome not (lookup_markup name)) false;
+fun is_markup kind name = (case lookup_markup name of Some k => k = kind | None => false);
 
 
 (* augment syntax *)
@@ -365,12 +368,16 @@
   opt_newline -- Scan.one T.is_begin_ignore --
     P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore -- opt_newline);
 
-val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
-val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
+fun markup_kind k = Scan.one (T.is_kind T.Command andf is_markup k o T.val_of);
+
+val markup = markup_kind Markup >> T.val_of;
+val markup_env = markup_kind MarkupEnv >> T.val_of;
+val verbatim = markup_kind Verbatim;
 
 val present_token =
   ignore_stuff >> K None ||
   (improper |-- markup -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_token ||
+    improper |-- markup_env -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_env_token ||
     (P.$$$ "--" >> K "cmt") -- P.!!!! (improper |-- P.text) >> Present.markup_token ||
     (improper -- verbatim) |-- P.!!!! (improper |-- P.text --| improper_end)
       >> Present.verbatim_token ||
@@ -482,8 +489,9 @@
 
 (*final declarations of this structure!*)
 val command = parser false None;
-val markup_command = parser false (Some true);
-val verbatim_command = parser false (Some false);
+val markup_command = parser false (Some Markup);
+val markup_env_command = parser false (Some MarkupEnv);
+val verbatim_command = parser false (Some Verbatim);
 val improper_command = parser true None;
 
 

--- a/src/Pure/Thy/latex.ML	Sat Apr 01 20:26:20 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Apr 03 14:00:16 2000 +0200
@@ -7,7 +7,8 @@
 
 signature LATEX =
 sig
-  datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
+  datatype token = Basic of OuterLex.token | Markup of string * string |
+    MarkupEnv of string * string | Verbatim of string
   val old_symbol_source: string -> Symbol.symbol list -> string
   val token_source: token list -> string
   val theory_entry: string -> string
@@ -57,7 +58,11 @@
 
 structure T = OuterLex;
 
-datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
+datatype token =
+  Basic of T.token |
+  Markup of string * string |
+  MarkupEnv of string * string |
+  Verbatim of string;
 
 
 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
@@ -80,6 +85,8 @@
         else output_syms s
       end
   | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
+  | output_tok (MarkupEnv (cmd, txt)) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
+      strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
 
 

--- a/src/Pure/Thy/present.ML	Sat Apr 01 20:26:20 2000 +0200
+++ b/src/Pure/Thy/present.ML	Mon Apr 03 14:00:16 2000 +0200
@@ -20,6 +20,7 @@
   type token
   val basic_token: OuterLex.token -> token
   val markup_token: string * string -> token
+  val markup_env_token: string * string -> token
   val verbatim_token: string -> token
   val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
   val token_source: string -> (unit -> token list) -> unit
@@ -375,6 +376,7 @@
 type token = Latex.token;
 val basic_token = Latex.Basic;
 val markup_token = Latex.Markup;
+val markup_env_token = Latex.MarkupEnv;
 val verbatim_token = Latex.Verbatim;
 
 fun old_symbol_source name mk_text =