# HG changeset patch
# User wenzelm
# Date 1552249888 -3600
# Node ID f752f3993db8359afd9baff76a8517070cbaf9d8
# Parent  def3ec9cdb7e06774013b523f7e301ef425e5d12
tuned -- Toplevel.presentation_context is total;

diff -r def3ec9cdb7e -r f752f3993db8 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Mar 10 21:12:29 2019 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Mar 10 21:31:28 2019 +0100
@@ -262,10 +262,7 @@
     val errs2 =
       (case result of
         NONE => []
-      | SOME st' =>
-          (case try Toplevel.presentation_context st' of
-            NONE => []
-          | SOME ctxt' => check_span_comments ctxt' span tr));
+      | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr);
     val errs = errs1 @ errs2;
     val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   in
diff -r def3ec9cdb7e -r f752f3993db8 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:12:29 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:31:28 2019 +0100
@@ -277,19 +277,17 @@
       in {tag' = tag', active_tag' = active_tag'} end
   end;
 
-fun present_span thy command_tag span state state'
+fun present_span command_tag span state state'
     (tag_stack, active_tag, newline, latex, present_cont) =
   let
-    val ctxt' =
-      Toplevel.presentation_context state'
-        handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
+    val ctxt' = Toplevel.presentation_context state';
     val present = fold (fn (tok, (flag, 0)) =>
         fold cons (present_token ctxt' tok)
         #> cons (Latex.string flag)
       | _ => I);
 
     val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
-    val cmd_tags = Document_Source.get_tags (Toplevel.presentation_context state');
+    val cmd_tags = Document_Source.get_tags ctxt';
 
     val (tag, tags) = tag_stack;
     val {tag', active_tag'} =
@@ -444,7 +442,7 @@
     val command_tag = make_command_tag options keywords;
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
+      Toplevel.setmp_thread_position tr (present_span command_tag span st st');
 
     fun present _ [] = I
       | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
diff -r def3ec9cdb7e -r f752f3993db8 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sun Mar 10 21:12:29 2019 +0100
+++ b/src/Pure/Tools/debugger.ML	Sun Mar 10 21:31:28 2019 +0100
@@ -279,8 +279,7 @@
             if Command.eval_finished eval then
               let
                 val st = Command.eval_result_state eval;
-                val ctxt = Toplevel.presentation_context st
-                  handle Toplevel.UNDEF => err ();
+                val ctxt = Toplevel.presentation_context st;
               in
                 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
                   SOME (b, _) => b := breakpoint_state