accomodate markup commands;

--- a/lib/texinputs/isabelle.sty	Wed Oct 06 00:34:48 1999 +0200
+++ b/lib/texinputs/isabelle.sty	Wed Oct 06 00:35:05 1999 +0200
@@ -6,8 +6,24 @@
 
 %%% Simple document preparation (based on theory token language)
 
+%basic environment
 \newenvironment{isabellesimple}{\small\tt\slshape\mbox{}}{}
 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
+
+%keywords
 \newcommand{\isacommand}[1]{{\bf #1}}
 \newcommand{\isakeyword}[1]{{\bf #1}}
-\newcommand{\isatext}[1]{{\rm #1}}
+
+%theory sections
+\newcommand{\isamarkupheader}[1]{{\rm #1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkuptext}[1]{{\rm #1}}
+
+%proof sections
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+\newcommand{\isamarkuptxt}[1]{{\sl #1}}

--- a/src/Pure/Thy/latex.ML	Wed Oct 06 00:34:48 1999 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Oct 06 00:35:05 1999 +0200
@@ -7,7 +7,7 @@
 
 signature LATEX =
 sig
-  val token_source: OuterLex.token list -> string
+  val token_source: (OuterLex.token * string option) list -> string
   val theory_entry: string -> string
 end;
 
@@ -17,8 +17,6 @@
 
 (* symbol output *)
 
-local
-
 val output_chr = fn
   " " => "~" |
   "\n" => "\\isanewline\n" |
@@ -31,54 +29,35 @@
   "}" => "{\\textbraceright}" |
   "~" => "{\\textasciitilde}" |
   "^" => "{\\textasciicircum}" |
-(*  "\"" => "{\\textquotedblleft}" |    (* FIXME !? *)*)
-  "\\" => "{\\textbackslash}" |
-(*  "|" => "{\\textbar}" |
-  "<" => "{\\textless}" |
-  ">" => "{\\textgreater}" |  *)
+  "\"" => "{\"}" |
+(*  "\\" => "{\\textbackslash}" |  FIXME *)
+  "\\" => "\\verb,\\," |
+  "|" => "{|}" |
+  "<" => "{<}" |
+  ">" => "{>}" |
   c => c;
 
-in
 
 (* FIXME replace \<forall> etc. *)
-val output_symbol = implode o map output_chr o explode;
-val output_symbols = map output_symbol;
-
-end;
+val output_sym = implode o map output_chr o explode;
+val output_symbols = map output_sym;
 
 
 (* token output *)
 
-local
-
 structure T = OuterLex;
 
-fun strip_blanks s =
-  implode (#1 (Library.take_suffix Symbol.is_blank
-    (#2 (Library.take_prefix Symbol.is_blank (explode s)))));
+fun output_tok (tok, Some s) = "\\isamarkup" ^ T.val_of tok ^ "{" ^ s ^ "}"
+  | output_tok (tok, None) =
+      let val s = T.val_of tok in
+        if T.is_kind T.Command tok then "\\isacommand{" ^ output_sym s ^ "}"
+        else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ output_sym s ^ "}"
+        else if T.is_kind T.String tok then output_sym (quote s)
+        else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
+        else output_sym s
+      end;
 
-fun output_tok tok =
-  let
-    val out = output_symbol;
-    val s = T.val_of tok;
-  in
-    if T.is_kind T.Command tok then "\\isacommand{" ^ out s ^ "}"
-    else if T.is_kind T.Keyword tok then "\\isakeyword{" ^ out s ^ "}"
-    else if T.is_kind T.String tok then out (quote s)
-    else if T.is_kind T.Verbatim tok then "\\isatext{" ^ strip_blanks s ^ "}"
-    else out s
-  end;
-
-(*adhoc tuning of tokens*)
-fun invisible_token tok =
-  T.is_kind T.Command tok andalso T.val_of tok mem_string ["text", "txt"] orelse
-  T.keyword_with (equal ";") tok orelse T.is_kind T.Comment tok;
-
-in
-
-val output_tokens = map output_tok o filter_out invisible_token;
-
-end;
+val output_tokens = map output_tok;
 
 
 (* theory presentation *)

--- a/src/Pure/Thy/present.ML	Wed Oct 06 00:34:48 1999 +0200
+++ b/src/Pure/Thy/present.ML	Wed Oct 06 00:35:05 1999 +0200
@@ -17,7 +17,7 @@
   val finish: unit -> unit
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> string list) -> unit
-  val token_source: string -> (unit -> OuterLex.token list) -> unit
+  val token_source: string -> (unit -> (OuterLex.token * string option) list) -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val result: string -> string -> thm -> unit
   val results: string -> string -> thm list -> unit