clarified presentation_state with provide presentation_context;
authorwenzelm
Tue Jan 09 17:58:35 2018 +0100 (17 months ago ago)
changeset 67390a256051dd3d6
parent 67389 7e21d19e7ad7
child 67391 d55e52e25d9a
clarified presentation_state with provide presentation_context;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jan 09 17:40:25 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jan 09 17:58:35 2018 +0100
     1.3 @@ -8,7 +8,6 @@
     1.4  sig
     1.5    exception UNDEF
     1.6    type state
     1.7 -  val generic_theory_toplevel: generic_theory -> state
     1.8    val theory_toplevel: theory -> state
     1.9    val toplevel: state
    1.10    val is_toplevel: state -> bool
    1.11 @@ -122,8 +121,7 @@
    1.12  
    1.13  datatype state = State of node option * node option;  (*current, previous*)
    1.14  
    1.15 -fun generic_theory_toplevel gthy = State (SOME (Theory (gthy, NONE)), NONE);
    1.16 -val theory_toplevel = generic_theory_toplevel o Context.Theory;
    1.17 +fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
    1.18  
    1.19  val toplevel = State (NONE, NONE);
    1.20  
    1.21 @@ -193,7 +191,7 @@
    1.22  
    1.23  fun presentation_state ctxt =
    1.24    (case Presentation_State.get ctxt of
    1.25 -    NONE => generic_theory_toplevel (Context.Proof ctxt)
    1.26 +    NONE => State (SOME (Theory (Context.Proof ctxt, SOME ctxt)), NONE)
    1.27    | SOME state => state);
    1.28  
    1.29