verbatim markup tokens;

--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 07 17:20:19 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 07 17:20:58 1999 +0200
@@ -58,7 +58,7 @@
 val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
   (P.comment >> (Toplevel.theory o IsarThy.add_text));
 
-val verbatimP = OuterSyntax.markup_command "verbatim" "verbatim document preparation text"
+val verbatimP = OuterSyntax.verbatim_command "verbatim" "verbatim document preparation text"
   K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_verbatim));
 
 
@@ -74,7 +74,7 @@
 val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
   (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
 
-val verbP = OuterSyntax.markup_command "verb" "verbatim document preparation text (proof)"
+val verbP = OuterSyntax.verbatim_command "verb" "verbatim document preparation text (proof)"
   K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_verb)));
 
 

--- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 17:20:19 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 17:20:58 1999 +0200
@@ -44,6 +44,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 verbatim_command: string -> string -> string ->
+    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val improper_command: string -> string -> string ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val dest_keywords: unit -> string list
@@ -100,7 +102,7 @@
 type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
 
 datatype parser =
-  Parser of string * (string * string * bool) * bool * parser_fn;
+  Parser of string * (string * string * bool option) * bool * parser_fn;
 
 fun parser int_only markup name comment kind parse =
   Parser (name, (comment, kind, markup), int_only, parse);
@@ -138,8 +140,8 @@
 
 val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
 val global_parsers =
-  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool) Symtab.table);
-val global_markups = ref ([]: string list);
+  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool option) Symtab.table);
+val global_markups = ref ([]: (string * bool) list);
 
 fun change_lexicons f =
   let val lexs = f (! global_lexicons) in
@@ -148,8 +150,8 @@
     | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
   end;
 
-fun get_markup (names, (name, (_, true))) = name :: names
-  | get_markup (names, _) = names;
+fun get_markup (ms, (name, (_, Some m))) = (name, m) :: ms
+  | get_markup (ms, _) = ms;
 
 fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
 fun change_parsers f = (global_parsers := f (! global_parsers); make_markups ());
@@ -165,7 +167,10 @@
 fun get_lexicons () = ! global_lexicons;
 fun get_parsers () = ! global_parsers;
 fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
-fun is_markup name = name mem_string ! global_markups;
+
+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;
 
 
 (* augment syntax *)
@@ -335,11 +340,14 @@
 
 val improper = Scan.any (not o T.is_proper);
 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);
 
 val present_token =
   improper |-- markup -- (improper |-- P.text --| (improper -- Scan.option semicolon -- improper))
     >> Present.markup_token ||
   (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
+  (improper -- verbatim -- improper) |-- P.text --| (improper -- Scan.option semicolon -- improper)
+    >> Present.verbatim_token ||
   Scan.one T.not_eof >> Present.basic_token;
 
 in
@@ -446,9 +454,10 @@
 
 
 (*final declarations of this structure!*)
-val command = parser false false;
-val markup_command = parser false true;
-val improper_command = parser true false;
+val command = parser false None;
+val markup_command = parser false (Some true);
+val verbatim_command = parser false (Some false);
+val improper_command = parser true None;
 
 
 end;

--- a/src/Pure/Thy/latex.ML	Thu Oct 07 17:20:19 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Oct 07 17:20:58 1999 +0200
@@ -7,7 +7,7 @@
 
 signature LATEX =
 sig
-  datatype token = Basic of OuterLex.token | Markup of string * string
+  datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
   val token_source: token list -> string
   val theory_entry: string -> string
 end;
@@ -51,7 +51,7 @@
 
 structure T = OuterLex;
 
-datatype token = Basic of T.token | Markup of string * string;
+datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
 
 
 val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
@@ -69,7 +69,8 @@
         else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
         else output_sym s
       end
-  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n";
+  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n"
+  | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n";
 
 
 val output_tokens = implode o map output_tok;

--- a/src/Pure/Thy/present.ML	Thu Oct 07 17:20:19 1999 +0200
+++ b/src/Pure/Thy/present.ML	Thu Oct 07 17:20:58 1999 +0200
@@ -20,6 +20,7 @@
   type token
   val basic_token: OuterLex.token -> token
   val markup_token: string * string -> token
+  val verbatim_token: string -> token
   val token_source: string -> (unit -> token list) -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val result: string -> string -> thm -> unit
@@ -355,6 +356,7 @@
 type token = Latex.token;
 val basic_token = Latex.Basic;
 val markup_token = Latex.Markup;
+val verbatim_token = Latex.Verbatim;
 
 fun token_source name mk_toks =
   with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));