tuned -- Toplevel.presentation_context is total;
authorwenzelm
Sun Mar 10 21:31:28 2019 +0100 (5 weeks ago ago)
changeset 70073f752f3993db8
parent 70072 def3ec9cdb7e
child 70074 1a7857abb75c
tuned -- Toplevel.presentation_context is total;
src/Pure/PIDE/command.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Sun Mar 10 21:12:29 2019 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Sun Mar 10 21:31:28 2019 +0100
     1.3 @@ -262,10 +262,7 @@
     1.4      val errs2 =
     1.5        (case result of
     1.6          NONE => []
     1.7 -      | SOME st' =>
     1.8 -          (case try Toplevel.presentation_context st' of
     1.9 -            NONE => []
    1.10 -          | SOME ctxt' => check_span_comments ctxt' span tr));
    1.11 +      | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr);
    1.12      val errs = errs1 @ errs2;
    1.13      val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
    1.14    in
     2.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:12:29 2019 +0100
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 10 21:31:28 2019 +0100
     2.3 @@ -277,19 +277,17 @@
     2.4        in {tag' = tag', active_tag' = active_tag'} end
     2.5    end;
     2.6  
     2.7 -fun present_span thy command_tag span state state'
     2.8 +fun present_span command_tag span state state'
     2.9      (tag_stack, active_tag, newline, latex, present_cont) =
    2.10    let
    2.11 -    val ctxt' =
    2.12 -      Toplevel.presentation_context state'
    2.13 -        handle Toplevel.UNDEF => Proof_Context.get_global thy Context.PureN;
    2.14 +    val ctxt' = Toplevel.presentation_context state';
    2.15      val present = fold (fn (tok, (flag, 0)) =>
    2.16          fold cons (present_token ctxt' tok)
    2.17          #> cons (Latex.string flag)
    2.18        | _ => I);
    2.19  
    2.20      val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
    2.21 -    val cmd_tags = Document_Source.get_tags (Toplevel.presentation_context state');
    2.22 +    val cmd_tags = Document_Source.get_tags ctxt';
    2.23  
    2.24      val (tag, tags) = tag_stack;
    2.25      val {tag', active_tag'} =
    2.26 @@ -444,7 +442,7 @@
    2.27      val command_tag = make_command_tag options keywords;
    2.28  
    2.29      fun present_command tr span st st' =
    2.30 -      Toplevel.setmp_thread_position tr (present_span thy command_tag span st st');
    2.31 +      Toplevel.setmp_thread_position tr (present_span command_tag span st st');
    2.32  
    2.33      fun present _ [] = I
    2.34        | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
     3.1 --- a/src/Pure/Tools/debugger.ML	Sun Mar 10 21:12:29 2019 +0100
     3.2 +++ b/src/Pure/Tools/debugger.ML	Sun Mar 10 21:31:28 2019 +0100
     3.3 @@ -279,8 +279,7 @@
     3.4              if Command.eval_finished eval then
     3.5                let
     3.6                  val st = Command.eval_result_state eval;
     3.7 -                val ctxt = Toplevel.presentation_context st
     3.8 -                  handle Toplevel.UNDEF => err ();
     3.9 +                val ctxt = Toplevel.presentation_context st;
    3.10                in
    3.11                  (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
    3.12                    SOME (b, _) => b := breakpoint_state