--- a/src/Pure/Thy/thy_output.ML Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Nov 06 15:47:04 2014 +0100
@@ -25,7 +25,7 @@
datatype markup = Markup | MarkupEnv | Verbatim
val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
val check_text: Symbol_Pos.source -> Toplevel.state -> unit
- val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) ->
+ val present_thy: Keyword.keywords -> (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
@@ -265,8 +265,7 @@
in
-fun present_span keywords default_tags span state state'
- (tag_stack, active_tag, newline, buffer, present_cont) =
+fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
let
val present = fold (fn (tok, (flag, 0)) =>
Buffer.add (output_token keywords state' tok)
@@ -281,7 +280,7 @@
val active_tag' =
if is_some tag' then tag'
else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
- else try hd (default_tags cmd_name);
+ else try hd (Keyword.command_tags keywords cmd_name);
val edge = (active_tag, active_tag');
val newline' =
@@ -351,7 +350,7 @@
in
-fun present_thy keywords default_tags is_markup command_results toks =
+fun present_thy keywords is_markup command_results toks =
let
(* tokens *)
@@ -423,7 +422,7 @@
(* present commands *)
fun present_command tr span st st' =
- Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st');
+ Toplevel.setmp_thread_position tr (present_span keywords span st st');
fun present _ [] = I
| present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;