src/Pure/Isar/toplevel.ML
author wenzelm
Sat Mar 29 19:14:13 2008 +0100 (2008-03-29 ago)
changeset 26491 c93ff30790fe
parent 26293 a71ea4a57f44
child 26602 5534b6a6b810
permissions -rw-r--r--
added generic_theory transaction;
     1 (*  Title:      Pure/Isar/toplevel.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The Isabelle/Isar toplevel.
     6 *)
     7 
     8 signature TOPLEVEL =
     9 sig
    10   exception UNDEF
    11   type generic_theory
    12   type node
    13   val theory_node: node -> generic_theory option
    14   val proof_node: node -> ProofHistory.T option
    15   val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
    16   val presentation_context: node option -> xstring option -> Proof.context
    17   type state
    18   val is_toplevel: state -> bool
    19   val is_theory: state -> bool
    20   val is_proof: state -> bool
    21   val level: state -> int
    22   val node_history_of: state -> node History.T
    23   val node_of: state -> node
    24   val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    25   val context_of: state -> Proof.context
    26   val generic_theory_of: state -> generic_theory
    27   val theory_of: state -> theory
    28   val proof_of: state -> Proof.state
    29   val proof_position_of: state -> int
    30   val enter_proof_body: state -> Proof.state
    31   val print_state_context: state -> unit
    32   val print_state: bool -> state -> unit
    33   val quiet: bool ref
    34   val debug: bool ref
    35   val interact: bool ref
    36   val timing: bool ref
    37   val profiling: int ref
    38   val skip_proofs: bool ref
    39   val crashes: exn list ref
    40   exception TERMINATE
    41   exception RESTART
    42   exception CONTEXT of Proof.context * exn
    43   exception TOPLEVEL_ERROR
    44   val exn_message: exn -> string
    45   val program: (unit -> 'a) -> 'a
    46   type transition
    47   val undo_limit: bool -> int option
    48   val empty: transition
    49   val name_of: transition -> string
    50   val source_of: transition -> OuterLex.token list option
    51   val name: string -> transition -> transition
    52   val position: Position.T -> transition -> transition
    53   val source: OuterLex.token list -> transition -> transition
    54   val interactive: bool -> transition -> transition
    55   val print: transition -> transition
    56   val print': string -> transition -> transition
    57   val three_buffersN: string
    58   val print3: transition -> transition
    59   val no_timing: transition -> transition
    60   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
    61     transition -> transition
    62   val init_empty: (state -> bool) -> (unit -> unit) -> transition -> transition
    63   val exit: transition -> transition
    64   val undo_exit: transition -> transition
    65   val kill: transition -> transition
    66   val history: (node History.T -> node History.T) -> transition -> transition
    67   val keep: (state -> unit) -> transition -> transition
    68   val keep': (bool -> state -> unit) -> transition -> transition
    69   val imperative: (unit -> unit) -> transition -> transition
    70   val theory: (theory -> theory) -> transition -> transition
    71   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    72   val theory': (bool -> theory -> theory) -> transition -> transition
    73   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
    74   val end_local_theory: transition -> transition
    75   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
    76   val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
    77   val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
    78     transition -> transition
    79   val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) ->
    80     transition -> transition
    81   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    82   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
    83   val forget_proof: transition -> transition
    84   val present_proof: (bool -> node -> unit) -> transition -> transition
    85   val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
    86   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    87   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
    88   val proof: (Proof.state -> Proof.state) -> transition -> transition
    89   val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    90   val skip_proof: (int History.T -> int History.T) -> transition -> transition
    91   val skip_proof_to_theory: (int -> bool) -> transition -> transition
    92   val unknown_theory: transition -> transition
    93   val unknown_proof: transition -> transition
    94   val unknown_context: transition -> transition
    95   val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
    96   val excursion: transition list -> unit
    97   val set_state: state -> unit
    98   val get_state: unit -> state
    99   val exn: unit -> (exn * string) option
   100   val >> : transition -> bool
   101   val >>> : transition list -> unit
   102   val init_state: unit -> unit
   103   type 'a isar
   104   val loop: bool -> 'a isar -> unit
   105 end;
   106 
   107 structure Toplevel: TOPLEVEL =
   108 struct
   109 
   110 
   111 (** toplevel state **)
   112 
   113 exception UNDEF;
   114 
   115 
   116 (* local theory wrappers *)
   117 
   118 type generic_theory = Context.generic;    (*theory or local_theory*)
   119 
   120 val loc_init = TheoryTarget.context;
   121 val loc_exit = ProofContext.theory_of o LocalTheory.exit;
   122 
   123 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   124   | loc_begin NONE (Context.Proof lthy) = lthy
   125   | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy);
   126 
   127 fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
   128   | loc_finish NONE (Context.Proof _) = Context.Proof o LocalTheory.restore
   129   | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
   130       Context.Proof (LocalTheory.reinit (LocalTheory.raw_theory (K (loc_exit lthy')) lthy));
   131 
   132 
   133 (* datatype node *)
   134 
   135 datatype node =
   136   Theory of generic_theory * Proof.context option | (*theory with presentation context*)
   137   Proof of ProofHistory.T * ((Proof.context -> generic_theory) * generic_theory) |
   138     (*history of proof states, finish, original theory*)
   139   SkipProof of int History.T * (generic_theory * generic_theory);
   140     (*history of proof depths, resulting theory, original theory*)
   141 
   142 val the_global_theory = fn Theory (Context.Theory thy, _) => thy | _ => raise UNDEF;
   143 val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE;
   144 val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
   145 
   146 fun cases_node f _ (Theory (gthy, _)) = f gthy
   147   | cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf)
   148   | cases_node f _ (SkipProof (_, (gthy, _))) = f gthy;
   149 
   150 fun presentation_context (SOME (Theory (_, SOME ctxt))) NONE = ctxt
   151   | presentation_context (SOME node) NONE = cases_node Context.proof_of Proof.context_of node
   152   | presentation_context (SOME node) (SOME loc) =
   153       loc_init loc (cases_node Context.theory_of Proof.theory_of node)
   154   | presentation_context NONE _ = raise UNDEF;
   155 
   156 
   157 (* datatype state *)
   158 
   159 type state_info = node History.T * ((theory -> unit) * (theory -> unit));
   160 
   161 datatype state =
   162   Toplevel of state_info option |  (*outer toplevel, leftover end state*)
   163   State of state_info;
   164 
   165 val toplevel = Toplevel NONE;
   166 
   167 fun is_toplevel (Toplevel _) = true
   168   | is_toplevel _ = false;
   169 
   170 fun level (Toplevel _) = 0
   171   | level (State (node, _)) =
   172       (case History.current node of
   173         Theory _ => 0
   174       | Proof (prf, _) => Proof.level (ProofHistory.current prf)
   175       | SkipProof (h, _) => History.current h + 1);   (*different notion of proof depth!*)
   176 
   177 fun str_of_state (Toplevel _) = "at top level"
   178   | str_of_state (State (node, _)) =
   179       (case History.current node of
   180         Theory (Context.Theory _, _) => "in theory mode"
   181       | Theory (Context.Proof _, _) => "in local theory mode"
   182       | Proof _ => "in proof mode"
   183       | SkipProof _ => "in skipped proof mode");
   184 
   185 
   186 (* top node *)
   187 
   188 fun node_history_of (Toplevel _) = raise UNDEF
   189   | node_history_of (State (node, _)) = node;
   190 
   191 val node_of = History.current o node_history_of;
   192 
   193 fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
   194 fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
   195 
   196 fun node_case f g state = cases_node f g (node_of state);
   197 
   198 val context_of = node_case Context.proof_of Proof.context_of;
   199 val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
   200 val theory_of = node_case Context.theory_of Proof.theory_of;
   201 val proof_of = node_case (fn _ => raise UNDEF) I;
   202 
   203 fun proof_position_of state =
   204   (case node_of state of
   205     Proof (prf, _) => ProofHistory.position prf
   206   | _ => raise UNDEF);
   207 
   208 val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
   209 
   210 
   211 (* print state *)
   212 
   213 val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
   214 
   215 fun print_state_context state =
   216   (case try node_of state of
   217     NONE => []
   218   | SOME (Theory (gthy, _)) => pretty_context gthy
   219   | SOME (Proof (_, (_, gthy))) => pretty_context gthy
   220   | SOME (SkipProof (_, (gthy, _))) => pretty_context gthy)
   221   |> Pretty.chunks |> Pretty.writeln;
   222 
   223 fun print_state prf_only state =
   224   (case try node_of state of
   225     NONE => []
   226   | SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy
   227   | SOME (Proof (prf, _)) =>
   228       Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
   229   | SOME (SkipProof (h, _)) =>
   230       [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))])
   231   |> Pretty.markup_chunks Markup.state |> Pretty.writeln;
   232 
   233 
   234 
   235 (** toplevel transitions **)
   236 
   237 val quiet = ref false;
   238 val debug = Output.debugging;
   239 val interact = ref false;
   240 val timing = Output.timing;
   241 val profiling = ref 0;
   242 val skip_proofs = ref false;
   243 val crashes = ref ([]: exn list);
   244 
   245 exception TERMINATE;
   246 exception RESTART;
   247 exception EXCURSION_FAIL of exn * string;
   248 exception FAILURE of state * exn;
   249 exception TOPLEVEL_ERROR;
   250 
   251 
   252 (* print exceptions *)
   253 
   254 exception CONTEXT of Proof.context * exn;
   255 
   256 fun exn_context NONE exn = exn
   257   | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
   258 
   259 local
   260 
   261 fun if_context NONE _ _ = []
   262   | if_context (SOME ctxt) f xs = map (f ctxt) xs;
   263 
   264 fun raised name [] = "exception " ^ name ^ " raised"
   265   | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
   266   | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
   267 
   268 in
   269 
   270 fun exn_message e =
   271   let
   272     val detailed = ! debug;
   273 
   274     fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
   275       | exn_msg ctxt (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg ctxt) exns)
   276       | exn_msg ctxt (Exn.EXCEPTIONS (exns, msg)) = cat_lines (map (exn_msg ctxt) exns @ [msg])
   277       | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
   278           exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
   279       | exn_msg _ TERMINATE = "Exit."
   280       | exn_msg _ RESTART = "Restart."
   281       | exn_msg _ Interrupt = "Interrupt."
   282       | exn_msg _ TimeLimit.TimeOut = "Timeout."
   283       | exn_msg _ TOPLEVEL_ERROR = "Error."
   284       | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
   285       | exn_msg _ (ERROR msg) = msg
   286       | exn_msg _ (Fail msg) = raised "Fail" [msg]
   287       | exn_msg _ (THEORY (msg, thys)) =
   288           raised "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
   289       | exn_msg _ (Syntax.AST (msg, asts)) = raised "AST" (msg ::
   290             (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
   291       | exn_msg ctxt (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
   292             (if detailed then
   293               if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
   294              else []))
   295       | exn_msg ctxt (TERM (msg, ts)) = raised "TERM" (msg ::
   296             (if detailed then if_context ctxt Syntax.string_of_term ts else []))
   297       | exn_msg ctxt (THM (msg, i, thms)) = raised ("THM " ^ string_of_int i) (msg ::
   298             (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
   299       | exn_msg _ exn = raised (General.exnMessage exn) []
   300   in exn_msg NONE e end;
   301 
   302 fun print_exn exn_info = Output.error_msg (exn_message (EXCURSION_FAIL exn_info));
   303 
   304 end;
   305 
   306 
   307 (* controlled execution *)
   308 
   309 local
   310 
   311 fun debugging f x =
   312   if ! debug then exception_trace (fn () => f x)
   313   else f x;
   314 
   315 fun toplevel_error f x =
   316   let val ctxt = try ML_Context.the_local_context () in
   317     f x handle exn =>
   318       (Output.error_msg (exn_message (exn_context ctxt exn)); raise TOPLEVEL_ERROR)
   319   end;
   320 
   321 in
   322 
   323 fun controlled_execution f =
   324   f
   325   |> debugging
   326   |> interruptible;
   327 
   328 fun program f =
   329  (f
   330   |> debugging
   331   |> toplevel_error) ();
   332 
   333 end;
   334 
   335 
   336 (* node transactions and recovery from stale theories *)
   337 
   338 (*NB: proof commands should be non-destructive!*)
   339 
   340 local
   341 
   342 fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
   343 
   344 val stale_theory = ERROR "Stale theory encountered after successful execution!";
   345 
   346 fun map_theory f = History.map_current
   347   (fn Theory (gthy, _) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, NONE)
   348     | node => node);
   349 
   350 fun return (result, NONE) = result
   351   | return (result, SOME exn) = raise FAILURE (result, exn);
   352 
   353 in
   354 
   355 fun transaction hist pos f (node, term) =
   356   let
   357     val cont_node = map_theory Theory.checkpoint node;
   358     val back_node = map_theory Theory.copy cont_node;
   359     fun state nd = State (nd, term);
   360     fun normal_state nd = (state nd, NONE);
   361     fun error_state nd exn = (state nd, SOME exn);
   362 
   363     val (result, err) =
   364       cont_node
   365       |> (f
   366           |> (if hist then History.apply' (History.current back_node) else History.map_current)
   367           |> controlled_execution)
   368       |> normal_state
   369       handle exn => error_state cont_node exn;
   370   in
   371     if is_stale result
   372     then return (error_state back_node (the_default stale_theory err))
   373     else return (result, err)
   374   end;
   375 
   376 end;
   377 
   378 
   379 (* primitive transitions *)
   380 
   381 (*Note: Recovery from stale theories is provided only for theory-level
   382   operations via Transaction.  Other node or state operations should
   383   not touch theories at all.  Interrupts are enabled only for Keep and
   384   Transaction.*)
   385 
   386 datatype trans =
   387   Init of (bool -> theory) * ((theory -> unit) * (theory -> unit)) |
   388                                                     (*init node; with exit/kill operation*)
   389   InitEmpty of (state -> bool) * (unit -> unit) |   (*init empty toplevel*)
   390   Exit |                                            (*conclude node -- deferred until init*)
   391   UndoExit |                                        (*continue after conclusion*)
   392   Kill |                                            (*abort node*)
   393   History of node History.T -> node History.T |     (*history operation (undo etc.)*)
   394   Keep of bool -> state -> unit |                   (*peek at state*)
   395   Transaction of bool * (bool -> node -> node);     (*node transaction*)
   396 
   397 fun undo_limit int = if int then NONE else SOME 0;
   398 
   399 fun safe_exit (Toplevel (SOME (node, (exit, _)))) =
   400     (case try the_global_theory (History.current node) of
   401       SOME thy => controlled_execution exit thy
   402     | NONE => ())
   403   | safe_exit _ = ();
   404 
   405 local
   406 
   407 fun keep_state int f = controlled_execution (fn x => tap (f int) x);
   408 
   409 fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
   410       let val node = Theory (Context.Theory (f int), NONE)
   411       in safe_exit state; State (History.init (undo_limit int) node, term) end
   412   | apply_tr int _ (InitEmpty (check, f)) (state as Toplevel _) =
   413       if check state then (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel)
   414       else raise UNDEF
   415   | apply_tr _ _ Exit (State (node, term)) =
   416       (the_global_theory (History.current node); Toplevel (SOME (node, term)))
   417   | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info
   418   | apply_tr _ _ Kill (State (node, (_, kill))) =
   419       (kill (the_global_theory (History.current node)); toplevel)
   420   | apply_tr _ _ (History f) (State (node, term)) = State (f node, term)
   421   | apply_tr int _ (Keep f) state = keep_state int f state
   422   | apply_tr int pos (Transaction (hist, f)) (State state) =
   423       transaction hist pos (fn x => f int x) state
   424   | apply_tr _ _ _ _ = raise UNDEF;
   425 
   426 fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
   427   | apply_union int pos (tr :: trs) state =
   428       apply_tr int pos tr state
   429         handle UNDEF => apply_union int pos trs state
   430           | FAILURE (alt_state, UNDEF) => apply_union int pos trs alt_state
   431           | exn as FAILURE _ => raise exn
   432           | exn => raise FAILURE (state, exn);
   433 
   434 in
   435 
   436 fun apply_trans int pos trs state = (apply_union int pos trs state, NONE)
   437   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
   438 
   439 end;
   440 
   441 
   442 (* datatype transition *)
   443 
   444 datatype transition = Transition of
   445  {name: string,                        (*command name*)
   446   pos: Position.T,                     (*source position*)
   447   source: OuterLex.token list option,  (*source text*)
   448   int_only: bool,                      (*interactive-only*)
   449   print: string list,                  (*print modes (union)*)
   450   no_timing: bool,                     (*suppress timing*)
   451   trans: trans list};                  (*primitive transitions (union)*)
   452 
   453 fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
   454   Transition {name = name, pos = pos, source = source,
   455     int_only = int_only, print = print, no_timing = no_timing, trans = trans};
   456 
   457 fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
   458   make_transition (f (name, pos, source, int_only, print, no_timing, trans));
   459 
   460 val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
   461 
   462 fun name_of (Transition {name, ...}) = name;
   463 fun source_of (Transition {source, ...}) = source;
   464 
   465 
   466 (* diagnostics *)
   467 
   468 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
   469 
   470 fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
   471 fun at_command tr = command_msg "At " tr ^ ".";
   472 
   473 fun type_error tr state =
   474   ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
   475 
   476 
   477 (* modify transitions *)
   478 
   479 fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
   480   (nm, pos, source, int_only, print, no_timing, trans));
   481 
   482 fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
   483   (name, pos, source, int_only, print, no_timing, trans));
   484 
   485 fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
   486   (name, pos, SOME src, int_only, print, no_timing, trans));
   487 
   488 fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
   489   (name, pos, source, int_only, print, no_timing, trans));
   490 
   491 val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
   492   (name, pos, source, int_only, print, true, trans));
   493 
   494 fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   495   (name, pos, source, int_only, print, no_timing, trans @ [tr]));
   496 
   497 fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   498   (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
   499 
   500 val print = print' "";
   501 
   502 val three_buffersN = "three_buffers";
   503 val print3 = print' three_buffersN;
   504 
   505 
   506 (* basic transitions *)
   507 
   508 fun init_theory f exit kill = add_trans (Init (f, (exit, kill)));
   509 fun init_empty check f = add_trans (InitEmpty (check, f));
   510 val exit = add_trans Exit;
   511 val undo_exit = add_trans UndoExit;
   512 val kill = add_trans Kill;
   513 val history = add_trans o History;
   514 val keep' = add_trans o Keep;
   515 fun map_current f = add_trans (Transaction (false, f));
   516 fun app_current f = add_trans (Transaction (true, f));
   517 
   518 fun keep f = add_trans (Keep (fn _ => f));
   519 fun imperative f = keep (fn _ => f ());
   520 
   521 val unknown_theory = imperative (fn () => warning "Unknown theory context");
   522 val unknown_proof = imperative (fn () => warning "Unknown proof context");
   523 val unknown_context = imperative (fn () => warning "Unknown context");
   524 
   525 
   526 (* theory transitions *)
   527 
   528 fun generic_theory f = app_current (fn _ =>
   529   (fn Theory (gthy, _) => Theory (f gthy, NONE)
   530     | _ => raise UNDEF));
   531 
   532 fun theory' f = app_current (fn int =>
   533   (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
   534     | _ => raise UNDEF));
   535 
   536 fun theory f = theory' (K f);
   537 
   538 fun begin_local_theory begin f = app_current (fn _ =>
   539   (fn Theory (Context.Theory thy, _) =>
   540         let
   541           val lthy = f thy;
   542           val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
   543         in Theory (gthy, SOME lthy) end
   544     | _ => raise UNDEF));
   545 
   546 val end_local_theory = app_current (fn _ =>
   547   (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
   548     | _ => raise UNDEF));
   549 
   550 local
   551 
   552 fun local_theory_presentation loc f g = app_current (fn int =>
   553   (fn Theory (gthy, _) =>
   554         let
   555           val finish = loc_finish loc gthy;
   556           val lthy' = f (loc_begin loc gthy);
   557         in Theory (finish lthy', SOME lthy') end
   558     | _ => raise UNDEF) #> tap (g int));
   559 
   560 in
   561 
   562 fun local_theory loc f = local_theory_presentation loc f (K I);
   563 fun present_local_theory loc g = local_theory_presentation loc I g;
   564 
   565 end;
   566 
   567 
   568 (* proof transitions *)
   569 
   570 fun end_proof f = map_current (fn int =>
   571   (fn Proof (prf, (finish, _)) =>
   572         let val state = ProofHistory.current prf in
   573           if can (Proof.assert_bottom true) state then
   574             let
   575               val ctxt' = f int state;
   576               val gthy' = finish ctxt';
   577             in Theory (gthy', SOME ctxt') end
   578           else raise UNDEF
   579         end
   580     | SkipProof (h, (gthy, _)) =>
   581         if History.current h = 0 then Theory (gthy, NONE) else raise UNDEF
   582     | _ => raise UNDEF));
   583 
   584 local
   585 
   586 fun begin_proof init finish = app_current (fn int =>
   587   (fn Theory (gthy, _) =>
   588     let
   589       val prf = init int gthy;
   590       val schematic = Proof.schematic_goal prf;
   591     in
   592       if ! skip_proofs andalso schematic then
   593         warning "Cannot skip proof of schematic goal statement"
   594       else ();
   595       if ! skip_proofs andalso not schematic then
   596         SkipProof
   597           (History.init (undo_limit int) 0, (finish gthy (Proof.global_skip_proof int prf), gthy))
   598       else Proof (ProofHistory.init (undo_limit int) prf, (finish gthy, gthy))
   599     end
   600   | _ => raise UNDEF));
   601 
   602 in
   603 
   604 fun local_theory_to_proof' loc f = begin_proof
   605   (fn int => fn gthy => f int (loc_begin loc gthy))
   606   (loc_finish loc);
   607 
   608 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
   609 
   610 fun theory_to_proof f = begin_proof
   611   (K (fn Context.Theory thy => f thy | _ => raise UNDEF))
   612   (K (Context.Theory o ProofContext.theory_of));
   613 
   614 end;
   615 
   616 val forget_proof = map_current (fn _ =>
   617   (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
   618     | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
   619     | _ => raise UNDEF));
   620 
   621 fun present_proof f = map_current (fn int =>
   622   (fn Proof (prf, x) => Proof (ProofHistory.apply I prf, x)
   623     | SkipProof (h, x) => SkipProof (History.apply I h, x)
   624     | _ => raise UNDEF) #> tap (f int));
   625 
   626 fun proofs' f = map_current (fn int =>
   627   (fn Proof (prf, x) => Proof (ProofHistory.applys (f int) prf, x)
   628     | SkipProof (h, x) => SkipProof (History.apply I h, x)
   629     | _ => raise UNDEF));
   630 
   631 fun proof' f = proofs' (Seq.single oo f);
   632 val proofs = proofs' o K;
   633 val proof = proof' o K;
   634 
   635 fun actual_proof f = map_current (fn _ =>
   636   (fn Proof (prf, x) => Proof (f prf, x)
   637     | _ => raise UNDEF));
   638 
   639 fun skip_proof f = map_current (fn _ =>
   640   (fn SkipProof (h, x) => SkipProof (f h, x)
   641     | _ => raise UNDEF));
   642 
   643 fun skip_proof_to_theory p = map_current (fn _ =>
   644   (fn SkipProof (h, (gthy, _)) =>
   645     if p (History.current h) then Theory (gthy, NONE)
   646     else raise UNDEF
   647   | _ => raise UNDEF));
   648 
   649 
   650 
   651 (** toplevel transactions **)
   652 
   653 (* thread position *)
   654 
   655 fun setmp_thread_position (Transition {pos, ...}) f x =
   656   Position.setmp_thread_data pos f x;
   657 
   658 
   659 (* apply transitions *)
   660 
   661 local
   662 
   663 fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) =
   664   setmp_thread_position tr (fn state =>
   665     let
   666       val _ =
   667         if not int andalso int_only then warning (command_msg "Interactive-only " tr)
   668         else ();
   669 
   670       fun do_timing f x = (warning (command_msg "" tr); timeap f x);
   671       fun do_profiling f x = profile (! profiling) f x;
   672 
   673       val (result, status) =
   674          state |> (apply_trans int pos trans
   675           |> (if ! profiling > 0 andalso not no_timing then do_profiling else I)
   676           |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
   677       val _ =
   678         if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ())
   679         then print_state false result else ();
   680 
   681     in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end);
   682 
   683 in
   684 
   685 fun apply int tr st =
   686   let val ctxt = try context_of st in
   687     (case app int tr st of
   688       (_, SOME TERMINATE) => NONE
   689     | (_, SOME RESTART) => SOME (toplevel, NONE)
   690     | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
   691     | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr))
   692     | (state', NONE) => SOME (state', NONE))
   693   end;
   694 
   695 end;
   696 
   697 
   698 (* excursion: toplevel -- apply transformers/presentation -- toplevel *)
   699 
   700 local
   701 
   702 fun excur [] x = x
   703   | excur ((tr, pr) :: trs) (st, res) =
   704       (case apply (! interact) tr st of
   705         SOME (st', NONE) =>
   706           excur trs (st', pr st st' res handle exn =>
   707             raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
   708       | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
   709       | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   710 
   711 fun no_pr _ _ _ = ();
   712 
   713 in
   714 
   715 fun present_excursion trs res =
   716   (case excur trs (toplevel, res) of
   717     (state as Toplevel _, res') => (safe_exit state; res')
   718   | _ => error "Unfinished development at end of input")
   719   handle exn => error (exn_message exn);
   720 
   721 fun excursion trs = present_excursion (map (rpair no_pr) trs) ();
   722 
   723 end;
   724 
   725 
   726 
   727 (** interactive transformations **)
   728 
   729 (* the global state reference *)
   730 
   731 val global_state = ref (toplevel, NONE: (exn * string) option);
   732 
   733 fun set_state state = global_state := (state, NONE);
   734 fun get_state () = fst (! global_state);
   735 fun exn () = snd (! global_state);
   736 
   737 
   738 (* apply transformers to global state --- NOT THREAD-SAFE! *)
   739 
   740 nonfix >> >>>;
   741 
   742 fun >> tr =
   743   (case apply true tr (get_state ()) of
   744     NONE => false
   745   | SOME (state', exn_info) =>
   746       (global_state := (state', exn_info);
   747         (case exn_info of
   748           NONE => ()
   749         | SOME err => setmp_thread_position tr print_exn err);
   750         true));
   751 
   752 fun >>> [] = ()
   753   | >>> (tr :: trs) = if >> tr then >>> trs else ();
   754 
   755 fun init_state () = (>> (init_empty (K true) (K ()) empty); ());
   756 
   757 
   758 (* the Isar source of transitions *)
   759 
   760 type 'a isar =
   761   (transition, (transition option,
   762     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
   763       Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
   764           Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
   765 
   766 local
   767 
   768 (*Spurious interrupts ahead!  Race condition?*)
   769 fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
   770 
   771 fun raw_loop secure src =
   772   let
   773     fun check_secure () =
   774       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
   775   in
   776     (case get_interrupt (Source.set_prompt Source.default_prompt src) of
   777       NONE => (writeln "\nInterrupt."; raw_loop secure src)
   778     | SOME NONE => if secure then quit () else ()
   779     | SOME (SOME (tr, src')) => if >> tr orelse check_secure () then raw_loop secure src' else ())
   780     handle exn => (Output.error_msg (exn_message exn) handle crash =>
   781       (CRITICAL (fn () => change crashes (cons crash));
   782         warning "Recovering after Isar toplevel crash -- see also Toplevel.crashes");
   783       raw_loop secure src)
   784   end;
   785 
   786 in
   787 
   788 fun loop secure src = uninterruptible (fn _ => raw_loop secure) src;
   789 
   790 end;
   791 
   792 end;