--- a/src/Pure/Thy/thy_output.ML Tue Sep 30 14:19:27 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Sep 30 14:19:28 2008 +0200
@@ -23,8 +23,8 @@
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list ref
val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
- val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
- Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
+ val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
+ (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
Proof.context -> 'a list -> string
val output: (Proof.context -> 'a -> Pretty.T) -> Args.src -> Proof.context -> 'a -> string
@@ -293,7 +293,7 @@
end;
-(* process_thy *)
+(* present_thy *)
datatype markup = Markup | MarkupEnv | Verbatim;
@@ -324,7 +324,7 @@
in
-fun process_thy lex default_tags is_markup trs src =
+fun present_thy lex default_tags is_markup command_results src =
let
(* tokens *)
@@ -390,10 +390,19 @@
|> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
|> Source.source stopper (Scan.error (Scan.bulk span)) NONE
|> Source.exhaust;
+
+
+ (* present commands *)
+
+ fun present_command tr span st st' =
+ Toplevel.setmp_thread_position tr (present_span lex default_tags span st st');
+
+ fun present _ [] = I
+ | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
in
- if length trs = length spans then
+ if length command_results = length spans then
((NONE, []), NONE, true, Buffer.empty, (I, I))
- |> Toplevel.present_excursion (trs ~~ map (present_span lex default_tags) spans)
+ |> present Toplevel.toplevel (command_results ~~ spans)
|> present_trailer
else error "Messed-up outer syntax for presentation"
end;