src/Pure/Isar/toplevel.ML
changeset 70059 ccc8e4c99520
parent 70058 45b2e784350a
child 70063 a9e574e2cba5
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 08 19:22:28 2019 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 08 21:18:58 2019 +0100
     1.3 @@ -101,27 +101,30 @@
     1.4  (* datatype node *)
     1.5  
     1.6  datatype node =
     1.7 -  Theory of generic_theory * Proof.context option
     1.8 -    (*theory with presentation context*) |
     1.9 +  Theory of generic_theory
    1.10 +    (*global or local theory*) |
    1.11    Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory)
    1.12      (*proof node, finish, original theory*) |
    1.13    Skipped_Proof of int * (generic_theory * generic_theory);
    1.14      (*proof depth, resulting theory, original theory*)
    1.15  
    1.16 -val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
    1.17 +val theory_node = fn Theory gthy => SOME gthy | _ => NONE;
    1.18  val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
    1.19  val skipped_proof_node = fn Skipped_Proof _ => true | _ => false;
    1.20  
    1.21 -fun cases_node f _ (Theory (gthy, _)) = f gthy
    1.22 +fun cases_node f _ (Theory gthy) = f gthy
    1.23    | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf)
    1.24    | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy;
    1.25  
    1.26  
    1.27  (* datatype state *)
    1.28  
    1.29 -datatype state = State of node option * node option;  (*current, previous*)
    1.30 +type node_presentation = node * Proof.context;  (*node with presentation context*)
    1.31 +fun node_presentation0 node = (node, cases_node Context.proof_of Proof.context_of node);
    1.32  
    1.33 -fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE);
    1.34 +datatype state = State of node_presentation option * node_presentation option; (*current, previous*)
    1.35 +
    1.36 +fun theory_toplevel thy = State (SOME (node_presentation0 (Theory (Context.Theory thy))), NONE);
    1.37  
    1.38  val toplevel = State (NONE, NONE);
    1.39  
    1.40 @@ -129,23 +132,23 @@
    1.41    | is_toplevel _ = false;
    1.42  
    1.43  fun level (State (NONE, _)) = 0
    1.44 -  | level (State (SOME (Theory _), _)) = 0
    1.45 -  | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
    1.46 -  | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
    1.47 +  | level (State (SOME (Theory _, _), _)) = 0
    1.48 +  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
    1.49 +  | level (State (SOME (Skipped_Proof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
    1.50  
    1.51 -fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy, _)))) =
    1.52 +fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy), _))) =
    1.53        "at top level, result theory " ^ quote (Context.theory_name thy)
    1.54    | str_of_state (State (NONE, _)) = "at top level"
    1.55 -  | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
    1.56 -  | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
    1.57 -  | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
    1.58 -  | str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode";
    1.59 +  | str_of_state (State (SOME (Theory (Context.Theory _), _), _)) = "in theory mode"
    1.60 +  | str_of_state (State (SOME (Theory (Context.Proof _), _), _)) = "in local theory mode"
    1.61 +  | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
    1.62 +  | str_of_state (State (SOME (Skipped_Proof _, _), _)) = "in skipped proof mode";
    1.63  
    1.64  
    1.65  (* current node *)
    1.66  
    1.67  fun node_of (State (NONE, _)) = raise UNDEF
    1.68 -  | node_of (State (SOME node, _)) = node;
    1.69 +  | node_of (State (SOME (node, _), _)) = node;
    1.70  
    1.71  fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
    1.72  fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
    1.73 @@ -154,7 +157,7 @@
    1.74  fun node_case f g state = cases_node f g (node_of state);
    1.75  
    1.76  fun previous_theory_of (State (_, NONE)) = NONE
    1.77 -  | previous_theory_of (State (_, SOME prev)) =
    1.78 +  | previous_theory_of (State (_, SOME (prev, _))) =
    1.79        SOME (cases_node Context.theory_of Proof.theory_of prev);
    1.80  
    1.81  val context_of = node_case Context.proof_of Proof.context_of;
    1.82 @@ -167,10 +170,10 @@
    1.83      Proof (prf, _) => Proof_Node.position prf
    1.84    | _ => ~1);
    1.85  
    1.86 -fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _, _)))) = true
    1.87 +fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _), _))) = true
    1.88    | is_end_theory _ = false;
    1.89  
    1.90 -fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    1.91 +fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy), _))) = thy
    1.92    | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
    1.93  
    1.94  
    1.95 @@ -183,10 +186,9 @@
    1.96  );
    1.97  
    1.98  fun presentation_context0 state =
    1.99 -  (case try node_of state of
   1.100 -    SOME (Theory (_, SOME ctxt)) => ctxt
   1.101 -  | SOME node => cases_node Context.proof_of Proof.context_of node
   1.102 -  | NONE =>
   1.103 +  (case state of
   1.104 +    State (SOME (_, ctxt), _) => ctxt
   1.105 +  | State (NONE, _) =>
   1.106        (case try Theory.get_pure () of
   1.107          SOME thy => Proof_Context.init_global thy
   1.108        | NONE => raise UNDEF));
   1.109 @@ -197,7 +199,7 @@
   1.110  
   1.111  fun presentation_state ctxt =
   1.112    (case Presentation_State.get ctxt of
   1.113 -    NONE => State (SOME (Theory (Context.Proof ctxt, SOME ctxt)), NONE)
   1.114 +    NONE => State (SOME (node_presentation0 (Theory (Context.Proof ctxt))), NONE)
   1.115    | SOME state => state);
   1.116  
   1.117  
   1.118 @@ -210,7 +212,7 @@
   1.119        let
   1.120          val gthy =
   1.121            (case node of
   1.122 -            Theory (gthy, _) => gthy
   1.123 +            Theory gthy => gthy
   1.124            | Proof (_, (_, gthy)) => gthy
   1.125            | Skipped_Proof (_, (_, gthy)) => gthy);
   1.126          val lthy = Context.cases Named_Target.theory_init I gthy;
   1.127 @@ -237,24 +239,17 @@
   1.128  
   1.129  exception FAILURE of state * exn;
   1.130  
   1.131 -local
   1.132 -
   1.133 -fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
   1.134 -  | reset_presentation node = node;
   1.135 -
   1.136 -in
   1.137 -
   1.138  fun apply_transaction f g node =
   1.139    let
   1.140 -    val cont_node = reset_presentation node;
   1.141 -    val context = cases_node I (Context.Proof o Proof.context_of) cont_node;
   1.142 -    fun state_error e nd = (State (SOME nd, SOME cont_node), e);
   1.143 +    val node_pr = node_presentation0 node;
   1.144 +    val context = cases_node I (Context.Proof o Proof.context_of) node;
   1.145 +    fun state_error e node_pr' = (State (SOME node_pr', SOME node_pr), e);
   1.146  
   1.147      val (result, err) =
   1.148 -      cont_node
   1.149 +      node
   1.150        |> Runtime.controlled_execution (SOME context) f
   1.151        |> state_error NONE
   1.152 -      handle exn => state_error (SOME exn) cont_node;
   1.153 +      handle exn => state_error (SOME exn) node_pr;
   1.154    in
   1.155      (case err of
   1.156        NONE => tap g result
   1.157 @@ -263,30 +258,34 @@
   1.158  
   1.159  val exit_transaction =
   1.160    apply_transaction
   1.161 -    (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
   1.162 -      | node => node) (K ())
   1.163 -  #> (fn State (node', _) => State (NONE, node'));
   1.164 -
   1.165 -end;
   1.166 +    ((fn Theory (Context.Theory thy) => Theory (Context.Theory (Theory.end_theory thy))
   1.167 +       | node => node) #> node_presentation0)
   1.168 +    (K ())
   1.169 +  #> (fn State (node_pr', _) => State (NONE, node_pr'));
   1.170  
   1.171  
   1.172  (* primitive transitions *)
   1.173  
   1.174  datatype trans =
   1.175 -  Init of unit -> theory |               (*init theory*)
   1.176 -  Exit |                                 (*formal exit of theory*)
   1.177 -  Keep of bool -> state -> unit |        (*peek at state*)
   1.178 -  Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
   1.179 +  (*init theory*)
   1.180 +  Init of unit -> theory |
   1.181 +  (*formal exit of theory*)
   1.182 +  Exit |
   1.183 +  (*peek at state*)
   1.184 +  Keep of bool -> state -> unit |
   1.185 +  (*node transaction and presentation*)
   1.186 +  Transaction of (bool -> node -> node_presentation) * (state -> unit);
   1.187  
   1.188  local
   1.189  
   1.190  fun apply_tr _ (Init f) (State (NONE, _)) =
   1.191 -      State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE)
   1.192 -  | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
   1.193 -      exit_transaction state
   1.194 +      let val node = Theory (Context.Theory (Runtime.controlled_execution NONE f ()))
   1.195 +      in State (SOME (node_presentation0 node), NONE) end
   1.196 +  | apply_tr _ Exit (State (SOME (node as Theory (Context.Theory _), _), _)) =
   1.197 +      exit_transaction node
   1.198    | apply_tr int (Keep f) state =
   1.199        Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   1.200 -  | apply_tr int (Transaction (f, g)) (State (SOME node, _)) =
   1.201 +  | apply_tr int (Transaction (f, g)) (State (SOME (node, _), _)) =
   1.202        apply_transaction (fn x => f int x) g node
   1.203    | apply_tr _ _ _ = raise UNDEF;
   1.204  
   1.205 @@ -369,6 +368,7 @@
   1.206  
   1.207  fun present_transaction f g = add_trans (Transaction (f, g));
   1.208  fun transaction f = present_transaction f (K ());
   1.209 +fun transaction0 f = present_transaction (node_presentation0 oo f) (K ());
   1.210  
   1.211  fun keep f = add_trans (Keep (fn _ => f));
   1.212  
   1.213 @@ -388,22 +388,22 @@
   1.214  (* theory transitions *)
   1.215  
   1.216  fun generic_theory f = transaction (fn _ =>
   1.217 -  (fn Theory (gthy, _) => Theory (f gthy, NONE)
   1.218 +  (fn Theory gthy => node_presentation0 (Theory (f gthy))
   1.219      | _ => raise UNDEF));
   1.220  
   1.221  fun theory' f = transaction (fn int =>
   1.222 -  (fn Theory (Context.Theory thy, _) =>
   1.223 +  (fn Theory (Context.Theory thy) =>
   1.224        let val thy' = thy
   1.225          |> Sign.new_group
   1.226          |> f int
   1.227          |> Sign.reset_group;
   1.228 -      in Theory (Context.Theory thy', NONE) end
   1.229 +      in node_presentation0 (Theory (Context.Theory thy')) end
   1.230      | _ => raise UNDEF));
   1.231  
   1.232  fun theory f = theory' (K f);
   1.233  
   1.234  fun begin_local_theory begin f = transaction (fn _ =>
   1.235 -  (fn Theory (Context.Theory thy, _) =>
   1.236 +  (fn Theory (Context.Theory thy) =>
   1.237          let
   1.238            val lthy = f thy;
   1.239            val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
   1.240 @@ -411,21 +411,21 @@
   1.241              (case Local_Theory.pretty lthy of
   1.242                [] => ()
   1.243              | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
   1.244 -        in Theory (gthy, SOME lthy) end
   1.245 +        in (Theory gthy, lthy) end
   1.246      | _ => raise UNDEF));
   1.247  
   1.248  val end_local_theory = transaction (fn _ =>
   1.249 -  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (Named_Target.exit lthy), SOME lthy)
   1.250 +  (fn Theory (Context.Proof lthy) => (Theory (Context.Theory (Named_Target.exit lthy)), lthy)
   1.251      | _ => raise UNDEF));
   1.252  
   1.253 -fun open_target f = transaction (fn _ =>
   1.254 -  (fn Theory (gthy, _) =>
   1.255 +fun open_target f = transaction0 (fn _ =>
   1.256 +  (fn Theory gthy =>
   1.257          let val lthy = f gthy
   1.258 -        in Theory (Context.Proof lthy, SOME lthy) end
   1.259 +        in Theory (Context.Proof lthy) end
   1.260      | _ => raise UNDEF));
   1.261  
   1.262  val close_target = transaction (fn _ =>
   1.263 -  (fn Theory (Context.Proof lthy, _) =>
   1.264 +  (fn Theory (Context.Proof lthy) =>
   1.265          (case try Local_Theory.close_target lthy of
   1.266            SOME ctxt' =>
   1.267              let
   1.268 @@ -433,7 +433,7 @@
   1.269                  if can Local_Theory.assert ctxt'
   1.270                  then Context.Proof ctxt'
   1.271                  else Context.Theory (Proof_Context.theory_of ctxt');
   1.272 -            in Theory (gthy', SOME lthy) end
   1.273 +            in (Theory gthy', lthy) end
   1.274          | NONE => raise UNDEF)
   1.275      | _ => raise UNDEF));
   1.276  
   1.277 @@ -442,7 +442,7 @@
   1.278    | restricted_context NONE = I;
   1.279  
   1.280  fun local_theory' restricted target f = present_transaction (fn int =>
   1.281 -  (fn Theory (gthy, _) =>
   1.282 +  (fn Theory gthy =>
   1.283          let
   1.284            val (finish, lthy) = Named_Target.switch target gthy;
   1.285            val lthy' = lthy
   1.286 @@ -450,16 +450,16 @@
   1.287              |> Local_Theory.new_group
   1.288              |> f int
   1.289              |> Local_Theory.reset_group;
   1.290 -        in Theory (finish lthy', SOME lthy') end
   1.291 +        in (Theory (finish lthy'), lthy') end
   1.292      | _ => raise UNDEF))
   1.293    (K ());
   1.294  
   1.295  fun local_theory restricted target f = local_theory' restricted target (K f);
   1.296  
   1.297  fun present_local_theory target = present_transaction (fn _ =>
   1.298 -  (fn Theory (gthy, _) =>
   1.299 +  (fn Theory gthy =>
   1.300          let val (finish, lthy) = Named_Target.switch target gthy;
   1.301 -        in Theory (finish lthy, SOME lthy) end
   1.302 +        in (Theory (finish lthy), lthy) end
   1.303      | _ => raise UNDEF));
   1.304  
   1.305  
   1.306 @@ -472,16 +472,16 @@
   1.307              let
   1.308                val ctxt' = f int state;
   1.309                val gthy' = finish ctxt';
   1.310 -            in Theory (gthy', SOME ctxt') end
   1.311 +            in (Theory gthy', ctxt') end
   1.312            else raise UNDEF
   1.313          end
   1.314 -    | Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
   1.315 +    | Skipped_Proof (0, (gthy, _)) => node_presentation0 (Theory gthy)
   1.316      | _ => raise UNDEF));
   1.317  
   1.318  local
   1.319  
   1.320 -fun begin_proof init = transaction (fn int =>
   1.321 -  (fn Theory (gthy, _) =>
   1.322 +fun begin_proof init = transaction0 (fn int =>
   1.323 +  (fn Theory gthy =>
   1.324      let
   1.325        val (finish, prf) = init int gthy;
   1.326        val document = Options.default_string "document";
   1.327 @@ -522,14 +522,14 @@
   1.328  
   1.329  end;
   1.330  
   1.331 -val forget_proof = transaction (fn _ =>
   1.332 +val forget_proof = transaction0 (fn _ =>
   1.333    (fn Proof (prf, (_, orig_gthy)) =>
   1.334          if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF
   1.335 -        else Theory (orig_gthy, NONE)
   1.336 -    | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
   1.337 +        else Theory orig_gthy
   1.338 +    | Skipped_Proof (_, (_, orig_gthy)) => Theory orig_gthy
   1.339      | _ => raise UNDEF));
   1.340  
   1.341 -fun proofs' f = transaction (fn int =>
   1.342 +fun proofs' f = transaction0 (fn int =>
   1.343    (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)
   1.344      | skip as Skipped_Proof _ => skip
   1.345      | _ => raise UNDEF));
   1.346 @@ -541,20 +541,20 @@
   1.347  
   1.348  (* skipped proofs *)
   1.349  
   1.350 -fun actual_proof f = transaction (fn _ =>
   1.351 +fun actual_proof f = transaction0 (fn _ =>
   1.352    (fn Proof (prf, x) => Proof (f prf, x)
   1.353      | _ => raise UNDEF));
   1.354  
   1.355 -fun skip_proof f = transaction (fn _ =>
   1.356 +fun skip_proof f = transaction0 (fn _ =>
   1.357    (fn skip as Skipped_Proof _ => (f (); skip)
   1.358      | _ => raise UNDEF));
   1.359  
   1.360 -val skip_proof_open = transaction (fn _ =>
   1.361 +val skip_proof_open = transaction0 (fn _ =>
   1.362    (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x)
   1.363      | _ => raise UNDEF));
   1.364  
   1.365 -val skip_proof_close = transaction (fn _ =>
   1.366 -  (fn Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE)
   1.367 +val skip_proof_close = transaction0 (fn _ =>
   1.368 +  (fn Skipped_Proof (0, (gthy, _)) => Theory gthy
   1.369      | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x)
   1.370      | _ => raise UNDEF));
   1.371  
   1.372 @@ -640,8 +640,8 @@
   1.373  
   1.374  val reset_proof =
   1.375    reset_state is_proof
   1.376 -    (transaction (fn _ =>
   1.377 -      (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy))
   1.378 +    (transaction0 (fn _ =>
   1.379 +      (fn Theory gthy => Skipped_Proof (0, (gthy, gthy))
   1.380          | _ => raise UNDEF)));
   1.381  
   1.382  val reset_notepad =
   1.383 @@ -725,10 +725,10 @@
   1.384                    {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1}
   1.385                    (fn () =>
   1.386                      let
   1.387 -                      val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
   1.388 -                      val prf' = Proof_Node.apply (K state) prf;
   1.389 +                      val State (SOME (Proof (prf, (_, orig_gthy)), _), prev) = st';
   1.390 +                      val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy));
   1.391                        val (result, result_state) =
   1.392 -                        State (SOME (Proof (prf', (finish, orig_gthy))), prev)
   1.393 +                        State (SOME (node_presentation0 node'), prev)
   1.394                          |> fold_map (element_result keywords) body_elems ||> command end_tr;
   1.395                      in (Result_List result, presentation_context0 result_state) end))
   1.396                #> (fn (res, state') => state' |> put_result (Result_Future res));