equal
deleted
inserted
replaced
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); |
112 |
112 |
113 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit |
113 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit |
114 | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore |
114 | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore |
115 | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => |
115 | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let |
116 Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy)); |
116 val target_name = #target (Named_Target.peek lthy); |
|
117 val target = if target_name = "" then NONE else SOME target_name; |
|
118 in Context.Proof (Named_Target.init target (loc_exit lthy')) end; |
117 |
119 |
118 |
120 |
119 (* datatype node *) |
121 (* datatype node *) |
120 |
122 |
121 datatype node = |
123 datatype node = |