src/Pure/Isar/toplevel.ML
changeset 62895 54c2abe7e9a4
parent 62889 99c7f31615c2
child 65054 9ad3f65c03f4
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 06 19:50:27 2016 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 06 23:45:19 2016 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    exception UNDEF
     1.6    type state
     1.7 +  val theory_toplevel: theory -> state
     1.8    val toplevel: state
     1.9    val is_toplevel: state -> bool
    1.10    val is_theory: state -> bool
    1.11 @@ -119,6 +120,8 @@
    1.12  
    1.13  datatype state = State of node option * node option;  (*current, previous*)
    1.14  
    1.15 +fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
    1.16 +
    1.17  val toplevel = State (NONE, NONE);
    1.18  
    1.19  fun is_toplevel (State (NONE, _)) = true