src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -23,9 +23,9 @@
   val boolean: string -> bool
   val integer: string -> int
   datatype markup = Markup | MarkupEnv | Verbatim
-  val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
+  val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
   val check_text: Symbol_Pos.source -> Toplevel.state -> unit
-  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
+  val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
@@ -158,9 +158,9 @@
 
 (* eval_antiq *)
 
-fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
+fun eval_antiq keywords state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
   let
-    val (opts, src) = Token.read_antiq lex antiq (ss, pos);
+    val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
     fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
     val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
     val print_ctxt = Context_Position.set_visible false preview_ctxt;
@@ -171,13 +171,13 @@
 
 (* check_text *)
 
-fun eval_antiquote lex state (txt, pos) =
+fun eval_antiquote keywords state (txt, pos) =
   let
     fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
       | words (Antiquote.Antiq _) = [];
 
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
-      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
+      | expand (Antiquote.Antiq antiq) = eval_antiq keywords state antiq;
 
     val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
     val _ = Position.reports (maps words ants);
@@ -190,7 +190,7 @@
 fun check_text {delimited, text, pos} state =
  (Position.report pos (Markup.language_document delimited);
   if Toplevel.is_skipped_proof state then ()
-  else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (text, pos)));
+  else ignore (eval_antiquote (Keyword.get_keywords ()) state (text, pos)));
 
 
 
@@ -207,8 +207,8 @@
   | MarkupEnvToken of string * (string * Position.T)
   | VerbatimToken of string * Position.T;
 
-fun output_token lex state =
-  let val eval = eval_antiquote lex state in
+fun output_token keywords state =
+  let val eval = eval_antiquote keywords state in
     fn NoToken => ""
      | BasicToken tok => Latex.output_basic tok
      | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
@@ -265,11 +265,11 @@
 
 in
 
-fun present_span lex default_tags span state state'
+fun present_span keywords default_tags span state state'
     (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (tok, (flag, 0)) =>
-        Buffer.add (output_token lex state' tok)
+        Buffer.add (output_token keywords state' tok)
         #> Buffer.add flag
       | _ => I);
 
@@ -351,7 +351,7 @@
 
 in
 
-fun present_thy lex default_tags is_markup command_results toks =
+fun present_thy keywords default_tags is_markup command_results toks =
   let
     (* tokens *)
 
@@ -423,7 +423,7 @@
     (* present commands *)
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span lex default_tags span st st');
+      Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st');
 
     fun present _ [] = I
       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;