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