equal
deleted
inserted
replaced
101 exception UNDEF = Runtime.UNDEF; |
101 exception UNDEF = Runtime.UNDEF; |
102 |
102 |
103 |
103 |
104 (* local theory wrappers *) |
104 (* local theory wrappers *) |
105 |
105 |
106 val loc_init = Theory_Target.context_cmd; |
106 val loc_init = Named_Target.context_cmd; |
107 val loc_exit = Local_Theory.exit_global; |
107 val loc_exit = Local_Theory.exit_global; |
108 |
108 |
109 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy |
109 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy |
110 | loc_begin NONE (Context.Proof lthy) = lthy |
110 | loc_begin NONE (Context.Proof lthy) = lthy |
111 | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); |
111 | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); |
192 | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos); |
192 | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos); |
193 |
193 |
194 |
194 |
195 (* print state *) |
195 (* print state *) |
196 |
196 |
197 val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I; |
197 val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I; |
198 |
198 |
199 fun print_state_context state = |
199 fun print_state_context state = |
200 (case try node_of state of |
200 (case try node_of state of |
201 NONE => [] |
201 NONE => [] |
202 | SOME (Theory (gthy, _)) => pretty_context gthy |
202 | SOME (Theory (gthy, _)) => pretty_context gthy |