src/Pure/Isar/toplevel.ML
changeset 37953 ddc3b72f9a42
parent 37951 4e2aaf080572
child 37977 3ceccd415145
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Jul 25 12:57:29 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Jul 25 14:41:48 2010 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val proof_of: state -> Proof.state
     1.5    val proof_position_of: state -> int
     1.6    val enter_proof_body: state -> Proof.state
     1.7 +  val end_theory: Position.T -> state -> theory
     1.8    val print_state_context: state -> unit
     1.9    val print_state: bool -> state -> unit
    1.10    val pretty_abstract: state -> Pretty.T
    1.11 @@ -45,7 +46,7 @@
    1.12    val interactive: bool -> transition -> transition
    1.13    val print: transition -> transition
    1.14    val no_timing: transition -> transition
    1.15 -  val init_theory: string -> (bool -> theory) -> (theory -> unit) -> transition -> transition
    1.16 +  val init_theory: string -> (bool -> theory) -> transition -> transition
    1.17    val exit: transition -> transition
    1.18    val keep: (state -> unit) -> transition -> transition
    1.19    val keep': (bool -> state -> unit) -> transition -> transition
    1.20 @@ -87,9 +88,8 @@
    1.21    val add_hook: (transition -> state -> state -> unit) -> unit
    1.22    val transition: bool -> transition -> state -> (state * (exn * string) option) option
    1.23    val run_command: string -> transition -> state -> state option
    1.24 -  val commit_exit: Position.T -> transition
    1.25    val command: transition -> state -> state
    1.26 -  val excursion: (transition * transition list) list -> (transition * state) list lazy
    1.27 +  val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
    1.28  end;
    1.29  
    1.30  structure Toplevel: TOPLEVEL =
    1.31 @@ -137,8 +137,7 @@
    1.32  
    1.33  (* datatype state *)
    1.34  
    1.35 -type node_info = node * (theory -> unit);  (*node with exit operation*)
    1.36 -datatype state = State of node_info option * node_info option;  (*current, previous*)
    1.37 +datatype state = State of node option * node option;  (*current, previous*)
    1.38  
    1.39  val toplevel = State (NONE, NONE);
    1.40  
    1.41 @@ -146,21 +145,21 @@
    1.42    | is_toplevel _ = false;
    1.43  
    1.44  fun level (State (NONE, _)) = 0
    1.45 -  | level (State (SOME (Theory _, _), _)) = 0
    1.46 -  | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf)
    1.47 -  | level (State (SOME (SkipProof (d, _), _), _)) = d + 1;   (*different notion of proof depth!*)
    1.48 +  | level (State (SOME (Theory _), _)) = 0
    1.49 +  | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
    1.50 +  | level (State (SOME (SkipProof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
    1.51  
    1.52  fun str_of_state (State (NONE, _)) = "at top level"
    1.53 -  | str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode"
    1.54 -  | str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode"
    1.55 -  | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode"
    1.56 -  | str_of_state (State (SOME (SkipProof _, _), _)) = "in skipped proof mode";
    1.57 +  | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
    1.58 +  | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
    1.59 +  | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
    1.60 +  | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode";
    1.61  
    1.62  
    1.63  (* current node *)
    1.64  
    1.65  fun node_of (State (NONE, _)) = raise UNDEF
    1.66 -  | node_of (State (SOME (node, _), _)) = node;
    1.67 +  | node_of (State (SOME node, _)) = node;
    1.68  
    1.69  fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
    1.70  fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
    1.71 @@ -174,7 +173,7 @@
    1.72    | NONE => raise UNDEF);
    1.73  
    1.74  fun previous_context_of (State (_, NONE)) = NONE
    1.75 -  | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
    1.76 +  | previous_context_of (State (_, SOME prev)) = SOME (context_node prev);
    1.77  
    1.78  val context_of = node_case Context.proof_of Proof.context_of;
    1.79  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
    1.80 @@ -188,6 +187,9 @@
    1.81  
    1.82  val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
    1.83  
    1.84 +fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
    1.85 +  | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
    1.86 +
    1.87  
    1.88  (* print state *)
    1.89  
    1.90 @@ -264,12 +266,12 @@
    1.91  
    1.92  in
    1.93  
    1.94 -fun apply_transaction f g (node, exit) =
    1.95 +fun apply_transaction f g node =
    1.96    let
    1.97      val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
    1.98      val cont_node = reset_presentation node;
    1.99      val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node;
   1.100 -    fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e);
   1.101 +    fun state_error e nd = (State (SOME nd, SOME node), e);
   1.102  
   1.103      val (result, err) =
   1.104        cont_node
   1.105 @@ -293,21 +295,18 @@
   1.106  (* primitive transitions *)
   1.107  
   1.108  datatype trans =
   1.109 -  Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*)
   1.110 -  Exit |                                         (*formal exit of theory -- without committing*)
   1.111 -  Commit_Exit |                                  (*exit and commit final theory*)
   1.112 -  Keep of bool -> state -> unit |                (*peek at state*)
   1.113 +  Init of string * (bool -> theory) |    (*theory name, init*)
   1.114 +  Exit |                                 (*formal exit of theory*)
   1.115 +  Keep of bool -> state -> unit |        (*peek at state*)
   1.116    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
   1.117  
   1.118  local
   1.119  
   1.120 -fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
   1.121 +fun apply_tr int (Init (_, f)) (State (NONE, _)) =
   1.122        State (SOME (Theory (Context.Theory
   1.123 -          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
   1.124 -  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
   1.125 +          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
   1.126 +  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
   1.127        State (NONE, prev)
   1.128 -  | apply_tr _ Commit_Exit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
   1.129 -      (Runtime.controlled_execution exit thy; toplevel)
   1.130    | apply_tr int (Keep f) state =
   1.131        Runtime.controlled_execution (fn x => tap (f int) x) state
   1.132    | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
   1.133 @@ -352,7 +351,7 @@
   1.134  
   1.135  (* diagnostics *)
   1.136  
   1.137 -fun init_of (Transition {trans = [Init (name, _, _)], ...}) = SOME name
   1.138 +fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
   1.139    | init_of _ = NONE;
   1.140  
   1.141  fun name_of (Transition {name, ...}) = name;
   1.142 @@ -394,7 +393,7 @@
   1.143  
   1.144  (* basic transitions *)
   1.145  
   1.146 -fun init_theory name f exit = add_trans (Init (name, f, exit));
   1.147 +fun init_theory name f = add_trans (Init (name, f));
   1.148  val exit = add_trans Exit;
   1.149  val keep' = add_trans o Keep;
   1.150  
   1.151 @@ -643,15 +642,6 @@
   1.152    | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
   1.153  
   1.154  
   1.155 -(* commit final exit *)
   1.156 -
   1.157 -fun commit_exit pos =
   1.158 -  name "end" empty
   1.159 -  |> position pos
   1.160 -  |> add_trans Commit_Exit
   1.161 -  |> imperative (fn () => warning "Expected to find finished theory");
   1.162 -
   1.163 -
   1.164  (* nested commands *)
   1.165  
   1.166  fun command tr st =
   1.167 @@ -693,8 +683,8 @@
   1.168            (fn prf =>
   1.169              Future.fork_pri ~1 (fn () =>
   1.170                let val (states, result_state) =
   1.171 -                (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
   1.172 -                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev))
   1.173 +                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
   1.174 +                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
   1.175                  |> fold_map command_result body_trs
   1.176                  ||> command (end_tr |> set_print false);
   1.177                in (states, presentation_context_of result_state) end))
   1.178 @@ -715,14 +705,9 @@
   1.179  fun excursion input =
   1.180    let
   1.181      val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
   1.182 -
   1.183      val immediate = not (Goal.future_enabled ());
   1.184      val (results, end_state) = fold_map (proof_result immediate) input toplevel;
   1.185 -    val _ =
   1.186 -      (case end_state of
   1.187 -        State (NONE, SOME (Theory (Context.Theory _, _), _)) =>
   1.188 -          command (commit_exit end_pos) end_state
   1.189 -      | _ => error "Unfinished development at end of input");
   1.190 -  in Lazy.lazy (fn () => maps Lazy.force results) end;
   1.191 +    val thy = end_theory end_pos end_state;
   1.192 +  in (Lazy.lazy (fn () => maps Lazy.force results), thy) end;
   1.193  
   1.194  end;