# HG changeset patch
# User wenzelm
# Date 1620830872 -7200
# Node ID 54fe8cc0e1c659dc9268ddf19ad5cd0457c71735
# Parent  b9aae426e51dca7ed3cc119e2ca621fd6d6e39f0
clarified signature: provide access to previous state;

diff -r b9aae426e51d -r 54fe8cc0e1c6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed May 12 14:55:51 2021 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed May 12 16:47:52 2021 +0200
@@ -88,7 +88,7 @@
   val reset_notepad: state -> state option
   val fork_presentation: transition -> transition * transition
   type result
-  val join_results: result -> (transition * state) list
+  val join_results: result -> (state * transition * state) list
   val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
 end;
 
@@ -693,9 +693,16 @@
   Result_List of result list |
   Result_Future of result future;
 
-fun join_results (Result x) = [x]
-  | join_results (Result_List xs) = maps join_results xs
-  | join_results (Result_Future x) = join_results (Future.join x);
+fun join_results result =
+  let
+    fun add (tr, st') res =
+      (case res of
+        [] => [(init_toplevel (), tr, st')]
+      | (_, _, st) :: _ => (st, tr, st') :: res);
+    fun acc (Result r) = add r
+      | acc (Result_List rs) = fold acc rs
+      | acc (Result_Future x) = acc (Future.join x);
+  in rev (acc result []) end;
 
 local
 
diff -r b9aae426e51d -r 54fe8cc0e1c6 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed May 12 14:55:51 2021 +0200
+++ b/src/Pure/PIDE/document.ML	Wed May 12 16:47:52 2021 +0200
@@ -738,13 +738,18 @@
               if Options.bool options "editor_presentation" then
                 let
                   val (_, offsets, rev_segments) =
-                    iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) =>
+                    iterate_entries (fn ((prev, _), opt_exec) => fn (offset, offsets, segments) =>
                       (case opt_exec of
                         SOME (eval, _) =>
                           let
                             val command_id = Command.eval_command_id eval;
                             val span = the_command_span command_id;
 
+                            val st =
+                              (case try (#1 o the o the_entry node o the) prev of
+                                NONE => Toplevel.init_toplevel ()
+                              | SOME prev_eval => Command.eval_result_state prev_eval);
+
                             val exec_id = Command.eval_exec_id eval;
                             val tr = Command.eval_result_command eval;
                             val st' = Command.eval_result_state eval;
@@ -753,14 +758,15 @@
                             val offsets' = offsets
                               |> Inttab.update (command_id, offset)
                               |> Inttab.update (exec_id, offset);
-                            val segments' = (span, tr, st') :: segments;
+                            val segments' = (span, (st, tr, st')) :: segments;
                           in SOME (offset', offsets', segments') end
                       | NONE => NONE)) node (0, Inttab.empty, []);
 
                   val adjust = Inttab.lookup offsets;
                   val segments =
-                    rev rev_segments |> map (fn (span, tr, st') =>
-                      {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
+                    rev rev_segments |> map (fn (span, (st, tr, st')) =>
+                      {span = Command_Span.adjust_offsets adjust span,
+                       prev_state = st, command = tr, state = st'});
 
                   val presentation_context: Thy_Info.presentation_context =
                    {options = options,
diff -r b9aae426e51d -r 54fe8cc0e1c6 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed May 12 14:55:51 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed May 12 16:47:52 2021 +0200
@@ -311,8 +311,9 @@
 
     fun present () =
       let
-        val segments = (spans ~~ maps Toplevel.join_results results)
-          |> map (fn (span, (tr, st')) => {span = span, command = tr, state = st'});
+        val segments =
+          (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) =>
+            {span = span, prev_state = st, command = tr, state = st'});
         val context: presentation_context =
           {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
       in apply_presentation context thy end;
diff -r b9aae426e51d -r 54fe8cc0e1c6 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed May 12 14:55:51 2021 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed May 12 16:47:52 2021 +0200
@@ -10,7 +10,9 @@
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val output_token: Proof.context -> Token.T -> Latex.text list
   val output_source: Proof.context -> string -> Latex.text list
-  type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
+  type segment =
+    {span: Command_Span.span, command: Toplevel.transition,
+     prev_state: Toplevel.state, state: Toplevel.state}
   val present_thy: Options.T -> theory -> segment list -> Latex.text list
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -357,7 +359,9 @@
 
 in
 
-type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
+type segment =
+  {span: Command_Span.span, command: Toplevel.transition,
+   prev_state: Toplevel.state, state: Toplevel.state};
 
 fun present_thy options thy (segments: segment list) =
   let