src/Pure/Isar/toplevel.ML
author wenzelm
Tue Jul 04 18:39:59 2006 +0200 (2006-07-04)
changeset 19996 a4332e71c1de
parent 19841 f2fa72c13186
child 20128 8f0e07d7cf92
permissions -rw-r--r--
skip_proofs: do not skip proofs of schematic goals (warning);
     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 node
    12   val theory_node: node -> theory option
    13   val proof_node: node -> ProofHistory.T option
    14   val cases_node: (theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
    15   val body_context_node: node option -> xstring option -> Proof.context
    16   type state
    17   val toplevel: 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 assert: bool -> unit
    23   val node_history_of: state -> node History.T
    24   val node_of: state -> node
    25   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    26   val context_of: state -> Context.generic
    27   val theory_of: state -> theory
    28   val proof_of: state -> Proof.state
    29   val proof_position_of: state -> int
    30   val enter_forward_proof: state -> Proof.state
    31   val prompt_state_default: state -> string
    32   val prompt_state_fn: (state -> string) ref
    33   val print_state_context: state -> unit
    34   val print_state_default: bool -> state -> unit
    35   val print_state_hook: (bool -> state -> unit) -> unit
    36   val print_state_fn: (bool -> state -> unit) ref
    37   val print_state: bool -> state -> unit
    38   val pretty_state: bool -> state -> Pretty.T list
    39   val quiet: bool ref
    40   val debug: bool ref
    41   val interact: bool ref
    42   val timing: bool ref
    43   val profiling: int ref
    44   val skip_proofs: bool ref
    45   exception TERMINATE
    46   exception RESTART
    47   val checkpoint: state -> state
    48   val copy: state -> state
    49   type transition
    50   val undo_limit: bool -> int option
    51   val empty: transition
    52   val name_of: transition -> string
    53   val source_of: transition -> OuterLex.token list option
    54   val name: string -> transition -> transition
    55   val position: Position.T -> transition -> transition
    56   val source: OuterLex.token list -> transition -> transition
    57   val interactive: bool -> transition -> transition
    58   val print: transition -> transition
    59   val print': string -> transition -> transition
    60   val three_buffersN: string
    61   val print3: transition -> transition
    62   val no_timing: transition -> transition
    63   val reset: transition -> transition
    64   val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
    65   val exit: transition -> transition
    66   val kill: transition -> transition
    67   val keep: (state -> unit) -> transition -> transition
    68   val keep': (bool -> state -> unit) -> transition -> transition
    69   val history: (node History.T -> node History.T) -> transition -> transition
    70   val imperative: (unit -> unit) -> transition -> transition
    71   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    72     -> transition -> transition
    73   val theory: (theory -> theory) -> transition -> transition
    74   val theory': (bool -> theory -> theory) -> transition -> transition
    75   val theory_context: (theory -> Proof.context * theory) -> transition -> transition
    76   val local_theory: xstring option -> (local_theory -> local_theory) ->
    77     transition -> transition
    78   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
    79   val proof: (Proof.state -> Proof.state) -> transition -> transition
    80   val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition
    81   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    82   val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition
    83   val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    84   val skip_proof: (int History.T -> int History.T) -> transition -> transition
    85   val proof_to_theory: (Proof.state -> theory) -> transition -> transition
    86   val proof_to_theory': (bool -> Proof.state -> theory) -> transition -> transition
    87   val proof_to_theory_context: (bool -> Proof.state -> Proof.context * theory)
    88     -> transition -> transition
    89   val skip_proof_to_theory: (int -> bool) -> transition -> transition
    90   val forget_proof: transition -> transition
    91   val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
    92   val present_proof: (bool -> node -> unit) -> transition -> transition
    93   val unknown_theory: transition -> transition
    94   val unknown_proof: transition -> transition
    95   val unknown_context: transition -> transition
    96   val exn_message: exn -> string
    97   val apply: bool -> transition -> state -> (state * (exn * string) option) option
    98   val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
    99   val excursion: transition list -> unit
   100   val program: (unit -> 'a) -> 'a
   101   val set_state: state -> unit
   102   val get_state: unit -> state
   103   val exn: unit -> (exn * string) option
   104   val >> : transition -> bool
   105   val >>> : transition list -> unit
   106   type 'a isar
   107   val loop: 'a isar -> unit
   108 end;
   109 
   110 structure Toplevel: TOPLEVEL =
   111 struct
   112 
   113 
   114 (** toplevel state **)
   115 
   116 exception UNDEF;
   117 
   118 
   119 (* datatype state *)
   120 
   121 datatype node =
   122   Theory of theory * Proof.context option |        (*theory with optional body context*)
   123   Proof of ProofHistory.T * theory |               (*history of proof states, original theory*)
   124   SkipProof of (int History.T * theory) * theory;
   125     (*history of proof depths, resulting theory, original theory*)
   126 
   127 val theory_node = fn Theory (thy, _) => SOME thy | _ => NONE;
   128 val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE;
   129 
   130 fun cases_node f _ (Theory (thy, _)) = f thy
   131   | cases_node _ g (Proof (prf, _)) = g (ProofHistory.current prf)
   132   | cases_node f _ (SkipProof ((_, thy), _)) = f thy;
   133 
   134 fun body_context_node (SOME (Theory (_, SOME ctxt))) NONE = ctxt
   135   | body_context_node (SOME node) loc =
   136       node |> cases_node (LocalTheory.init loc)
   137        (if is_some loc then LocalTheory.init loc o Proof.theory_of
   138         else Proof.context_of)
   139   | body_context_node NONE _ = raise UNDEF;
   140 
   141 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
   142 
   143 val toplevel = State NONE;
   144 
   145 fun is_toplevel (State NONE) = true
   146   | is_toplevel _ = false;
   147 
   148 fun level (State NONE) = 0
   149   | level (State (SOME (node, _))) =
   150       (case History.current node of
   151         Theory _ => 0
   152       | Proof (prf, _) => Proof.level (ProofHistory.current prf)
   153       | SkipProof ((h, _), _) => History.current h + 1);    (*different notion of proof depth!*)
   154 
   155 fun str_of_state (State NONE) = "at top level"
   156   | str_of_state (State (SOME (node, _))) =
   157       (case History.current node of
   158         Theory _ => "in theory mode"
   159       | Proof _ => "in proof mode"
   160       | SkipProof _ => "in skipped proof mode");
   161 
   162 
   163 (* top node *)
   164 
   165 fun assert true = ()
   166   | assert false = raise UNDEF;
   167 
   168 fun node_history_of (State NONE) = raise UNDEF
   169   | node_history_of (State (SOME (node, _))) = node;
   170 
   171 val node_of = History.current o node_history_of;
   172 
   173 fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state));
   174 fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state));
   175 
   176 fun node_case f g state = cases_node f g (node_of state);
   177 
   178 val context_of = node_case Context.Theory (Context.Proof o Proof.context_of);
   179 val theory_of = node_case I Proof.theory_of;
   180 val proof_of = node_case (fn _ => raise UNDEF) I;
   181 
   182 fun proof_position_of state =
   183   (case node_of state of
   184     Proof (prf, _) => ProofHistory.position prf
   185   | _ => raise UNDEF);
   186 
   187 val enter_forward_proof = node_case (Proof.init o ProofContext.init) Proof.enter_forward;
   188 
   189 
   190 (* prompt state *)
   191 
   192 fun prompt_state_default (State _) = Source.default_prompt;
   193 
   194 val prompt_state_fn = ref prompt_state_default;
   195 fun prompt_state state = ! prompt_state_fn state;
   196 
   197 
   198 (* print state *)
   199 
   200 fun pretty_context thy = [Pretty.block
   201   [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
   202     Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
   203 
   204 fun pretty_state_context state =
   205   (case try theory_of state of NONE => []
   206   | SOME thy => pretty_context thy);
   207 
   208 fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy
   209   | pretty_node _ (Proof (prf, _)) =
   210       Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf)
   211   | pretty_node _ (SkipProof ((h, _), _)) =
   212       [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))];
   213 
   214 fun pretty_state prf_only state =
   215   let val ref (begin_state, end_state, _) = Display.current_goals_markers in
   216     (case try node_of state of NONE => []
   217     | SOME node =>
   218         (if begin_state = "" then [] else [Pretty.str begin_state]) @
   219         pretty_node prf_only node @
   220         (if end_state = "" then [] else [Pretty.str end_state]))
   221   end;
   222 
   223 val print_state_context = Pretty.writelns o pretty_state_context;
   224 fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
   225 
   226 val print_state_hooks = ref ([]: (bool -> state -> unit) list);
   227 fun print_state_hook f = change print_state_hooks (cons f);
   228 val print_state_fn = ref print_state_default;
   229 
   230 fun print_state prf_only state =
   231  (List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks);
   232   ! print_state_fn prf_only state);
   233 
   234 
   235 
   236 (** toplevel transitions **)
   237 
   238 val quiet = ref false;
   239 val debug = ref false;
   240 val interact = ref false;
   241 val timing = Output.timing;
   242 val profiling = ref 0;
   243 val skip_proofs = ref false;
   244 
   245 exception TERMINATE;
   246 exception RESTART;
   247 exception EXCURSION_FAIL of exn * string;
   248 exception FAILURE of state * exn;
   249 
   250 fun debugging f x =
   251   if ! debug then
   252     setmp Library.do_transform_failure false
   253       exception_trace (fn () => f x)
   254   else f x;
   255 
   256 
   257 (* node transactions and recovery from stale theories *)
   258 
   259 (*NB: proof commands should be non-destructive!*)
   260 
   261 local
   262 
   263 fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
   264 
   265 val stale_theory = ERROR "Stale theory encountered after succesful execution!";
   266 
   267 fun checkpoint_node (Theory (thy, _)) = Theory (Theory.checkpoint thy, NONE)
   268   | checkpoint_node node = node;
   269 
   270 fun copy_node (Theory (thy, _)) = Theory (Theory.copy thy, NONE)
   271   | copy_node node = node;
   272 
   273 fun return (result, NONE) = result
   274   | return (result, SOME exn) = raise FAILURE (result, exn);
   275 
   276 fun interruptible f x =
   277   let val y = ref x
   278   in raise_interrupt (fn () => y := f x) (); ! y end;
   279 
   280 in
   281 
   282 fun transaction _ _ (State NONE) = raise UNDEF
   283   | transaction hist f (State (SOME (node, term))) =
   284       let
   285         val cont_node = History.map checkpoint_node node;
   286         val back_node = History.map copy_node cont_node;
   287         fun state nd = State (SOME (nd, term));
   288         fun normal_state nd = (state nd, NONE);
   289         fun error_state nd exn = (state nd, SOME exn);
   290 
   291         val (result, err) =
   292           cont_node
   293           |> (f
   294               |> (if hist then History.apply_copy copy_node else History.map)
   295               |> debugging
   296               |> interruptible
   297               |> setmp Output.do_toplevel_errors false)
   298           |> normal_state
   299           handle exn => error_state cont_node exn;
   300       in
   301         if is_stale result
   302         then return (error_state back_node (the_default stale_theory err))
   303         else return (result, err)
   304       end;
   305 
   306 fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term))
   307   | mapping _ state = state;
   308 
   309 val checkpoint = mapping checkpoint_node;
   310 val copy = mapping copy_node;
   311 
   312 end;
   313 
   314 
   315 (* primitive transitions *)
   316 
   317 (*Note: Recovery from stale theories is provided only for theory-level
   318   operations via Transaction.  Other node or state operations should
   319   not touch theories at all.  Interrupts are enabled only for Keep and
   320   Transaction.*)
   321 
   322 datatype trans =
   323   Reset |                                               (*empty toplevel*)
   324   Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
   325                                                         (*init node; with exit/kill operation*)
   326   Exit |                                                (*conclude node*)
   327   Kill |                                                (*abort node*)
   328   Keep of bool -> state -> unit |                       (*peek at state*)
   329   History of node History.T -> node History.T |         (*history operation (undo etc.)*)
   330   Transaction of bool * (bool -> node -> node);         (*node transaction*)
   331 
   332 fun undo_limit int = if int then NONE else SOME 0;
   333 
   334 local
   335 
   336 fun apply_tr _ Reset _ = toplevel
   337   | apply_tr int (Init (f, term)) (State NONE) =
   338       State (SOME (History.init (undo_limit int) (f int), term))
   339   | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF
   340   | apply_tr _ Exit (State NONE) = raise UNDEF
   341   | apply_tr _ Exit (State (SOME (node, (exit, _)))) =
   342       (exit (History.current node); State NONE)
   343   | apply_tr _ Kill (State NONE) = raise UNDEF
   344   | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
   345       (kill (History.current node); State NONE)
   346   | apply_tr int (Keep f) state =
   347       (setmp Output.do_toplevel_errors false (raise_interrupt (f int)) state; state)
   348   | apply_tr _ (History _) (State NONE) = raise UNDEF
   349   | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
   350   | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state;
   351 
   352 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   353   | apply_union int (tr :: trs) state =
   354       apply_tr int tr state
   355         handle UNDEF => apply_union int trs state
   356           | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
   357           | exn as FAILURE _ => raise exn
   358           | exn => raise FAILURE (state, exn);
   359 
   360 in
   361 
   362 fun apply_trans int trs state = (apply_union int trs state, NONE)
   363   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
   364 
   365 end;
   366 
   367 
   368 (* datatype transition *)
   369 
   370 datatype transition = Transition of
   371  {name: string,                        (*command name*)
   372   pos: Position.T,                     (*source position*)
   373   source: OuterLex.token list option,  (*source text*)
   374   int_only: bool,                      (*interactive-only*)
   375   print: string list,                  (*print modes (union)*)
   376   no_timing: bool,                     (*suppress timing*)
   377   trans: trans list};                  (*primitive transitions (union)*)
   378 
   379 fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
   380   Transition {name = name, pos = pos, source = source,
   381     int_only = int_only, print = print, no_timing = no_timing, trans = trans};
   382 
   383 fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
   384   make_transition (f (name, pos, source, int_only, print, no_timing, trans));
   385 
   386 val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
   387 
   388 fun name_of (Transition {name, ...}) = name;
   389 fun source_of (Transition {source, ...}) = source;
   390 
   391 
   392 (* diagnostics *)
   393 
   394 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
   395 
   396 fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
   397 fun at_command tr = command_msg "At " tr ^ ".";
   398 
   399 fun type_error tr state =
   400   ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
   401 
   402 
   403 (* modify transitions *)
   404 
   405 fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
   406   (nm, pos, source, int_only, print, no_timing, trans));
   407 
   408 fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
   409   (name, pos, source, int_only, print, no_timing, trans));
   410 
   411 fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
   412   (name, pos, SOME src, int_only, print, no_timing, trans));
   413 
   414 fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
   415   (name, pos, source, int_only, print, no_timing, trans));
   416 
   417 val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
   418   (name, pos, source, int_only, print, true, trans));
   419 
   420 fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   421   (name, pos, source, int_only, print, no_timing, trans @ [tr]));
   422 
   423 fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   424   (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
   425 
   426 val print = print' "";
   427 
   428 val three_buffersN = "three_buffers";
   429 val print3 = print' three_buffersN;
   430 
   431 
   432 (* build transitions *)
   433 
   434 val reset = add_trans Reset;
   435 fun init f exit kill = add_trans (Init (f, (exit, kill)));
   436 val exit = add_trans Exit;
   437 val kill = add_trans Kill;
   438 val keep' = add_trans o Keep;
   439 val history = add_trans o History;
   440 fun map_current f = add_trans (Transaction (false, f));
   441 fun app_current f = add_trans (Transaction (true, f));
   442 
   443 fun keep f = add_trans (Keep (fn _ => f));
   444 fun imperative f = keep (fn _ => f ());
   445 
   446 fun init_theory f exit kill =
   447   init (fn int => Theory (f int, NONE))
   448     (fn Theory (thy, _) => exit thy | _ => raise UNDEF)
   449     (fn Theory (thy, _) => kill thy | _ => raise UNDEF);
   450 
   451 
   452 (* typed transitions *)
   453 
   454 fun theory f = app_current
   455   (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF));
   456 
   457 fun theory' f = app_current (fn int =>
   458   (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
   459 
   460 fun theory_context f = app_current
   461   (K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy))) | _ => raise UNDEF));
   462 
   463 fun local_theory loc f = theory_context (LocalTheory.mapping loc f);
   464 
   465 fun theory_to_proof f = app_current (fn int =>
   466   (fn Theory (thy, _) =>
   467     let
   468       val prf = f thy;
   469       val schematic = Proof.schematic_goal prf;
   470     in
   471       if ! skip_proofs andalso schematic then
   472         warning "Cannot skip proof of schematic goal statement"
   473       else ();
   474       if ! skip_proofs andalso not schematic then
   475         SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
   476       else Proof (ProofHistory.init (undo_limit int) prf, thy)
   477     end
   478   | _ => raise UNDEF));
   479 
   480 fun proofs' f = map_current (fn int =>
   481   (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)
   482     | SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy)
   483     | _ => raise UNDEF));
   484 
   485 fun proof' f = proofs' (Seq.single oo f);
   486 val proofs = proofs' o K;
   487 val proof = proof' o K;
   488 
   489 fun actual_proof f = map_current (fn _ =>
   490   (fn Proof (prf, orig_thy) => Proof (f prf, orig_thy) | _ => raise UNDEF));
   491 
   492 fun skip_proof f = map_current (fn _ =>
   493   (fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy) | _ => raise UNDEF));
   494 
   495 fun end_proof f = map_current (fn int =>
   496   (fn Proof (prf, _) => Theory (f int (ProofHistory.current prf))
   497     | SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF
   498     | _ => raise UNDEF));
   499 
   500 val forget_proof = map_current (fn _ =>
   501   (fn Proof (_, orig_thy) => Theory (orig_thy, NONE)
   502     | SkipProof (_, orig_thy) => Theory (orig_thy, NONE)
   503     | _ => raise UNDEF));
   504 
   505 fun proof_to_theory' f = end_proof (rpair NONE oo f);
   506 fun proof_to_theory f = proof_to_theory' (K f);
   507 fun proof_to_theory_context f = end_proof ((swap o apfst SOME) oo f);
   508 
   509 fun skip_proof_to_theory p = map_current (fn _ =>
   510   (fn SkipProof ((h, thy), _) =>
   511     if p (History.current h) then Theory (thy, NONE)
   512     else raise UNDEF
   513   | _ => raise UNDEF));
   514 
   515 fun present_local_theory loc f = app_current (fn int =>
   516   (fn Theory (thy, _) => Theory (swap (apfst SOME (LocalTheory.mapping loc I thy)))
   517     | _ => raise UNDEF) #> tap (f int));
   518 
   519 fun present_proof f = map_current (fn int =>
   520   (fn node as Proof _ => node | _ => raise UNDEF) #> tap (f int));
   521 
   522 val unknown_theory = imperative (fn () => warning "Unknown theory context");
   523 val unknown_proof = imperative (fn () => warning "Unknown proof context");
   524 val unknown_context = imperative (fn () => warning "Unknown context");
   525 
   526 
   527 
   528 (** toplevel transactions **)
   529 
   530 (* print exceptions *)
   531 
   532 local
   533 
   534 fun with_context f xs =
   535   (case Context.get_context () of NONE => []
   536   | SOME thy => map (f thy) xs);
   537 
   538 fun raised name [] = "exception " ^ name ^ " raised"
   539   | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
   540   | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
   541 
   542 fun exn_msg _ TERMINATE = "Exit."
   543   | exn_msg _ RESTART = "Restart."
   544   | exn_msg _ Interrupt = "Interrupt."
   545   | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
   546   | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
   547   | exn_msg _ (ERROR msg) = msg
   548   | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   549   | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   550   | exn_msg false (THEORY (msg, _)) = msg
   551   | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
   552   | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
   553       fail_msg detailed "simproc" ((name, Position.none), exn)
   554   | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
   555   | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
   556   | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
   557   | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
   558   | exn_msg true (Syntax.AST (msg, asts)) =
   559       raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
   560   | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
   561   | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
   562         with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
   563   | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
   564   | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
   565   | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
   566   | exn_msg true (THM (msg, i, thms)) =
   567       raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
   568   | exn_msg _ Option.Option = raised "Option" []
   569   | exn_msg _ Library.UnequalLengths = raised "UnequalLengths" []
   570   | exn_msg _ Empty = raised "Empty" []
   571   | exn_msg _ Subscript = raised "Subscript" []
   572   | exn_msg _ (Fail msg) = raised "Fail" [msg]
   573   | exn_msg _ exn = General.exnMessage exn
   574 and fail_msg detailed kind ((name, pos), exn) =
   575   "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
   576 
   577 in
   578 
   579 fun exn_message exn = exn_msg (! debug) exn;
   580 
   581 fun print_exn NONE = ()
   582   | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
   583 
   584 end;
   585 
   586 
   587 (* apply transitions *)
   588 
   589 local
   590 
   591 fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
   592   let
   593     val _ = conditional (not int andalso int_only) (fn () =>
   594       warning (command_msg "Interactive-only " tr));
   595 
   596     fun do_timing f x = (Output.info (command_msg "" tr); timeap f x);
   597     fun do_profiling f x = profile (! profiling) f x;
   598 
   599     val (result, opt_exn) =
   600        state |> (apply_trans int trans
   601         |> (if ! profiling > 0 then do_profiling else I)
   602         |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
   603     val _ = conditional (int andalso not (! quiet) andalso
   604         exists (fn m => m mem_string print) ("" :: ! print_mode))
   605       (fn () => print_state false result);
   606   in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
   607 
   608 in
   609 
   610 fun apply int tr st =
   611   (case app int tr st of
   612     (_, SOME TERMINATE) => NONE
   613   | (_, SOME RESTART) => SOME (toplevel, NONE)
   614   | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
   615   | (state', SOME exn) => SOME (state', SOME (exn, at_command tr))
   616   | (state', NONE) => SOME (state', NONE));
   617 
   618 end;
   619 
   620 
   621 (* excursion: toplevel -- apply transformers/presentation -- toplevel *)
   622 
   623 local
   624 
   625 fun excur [] x = x
   626   | excur ((tr, pr) :: trs) (st, res) =
   627       (case apply (! interact) tr st of
   628         SOME (st', NONE) =>
   629           excur trs (st', pr st st' res handle exn =>
   630             raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
   631       | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
   632       | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   633 
   634 fun no_pr _ _ _ = ();
   635 
   636 in
   637 
   638 fun present_excursion trs res =
   639   (case excur trs (State NONE, res) of
   640     (State NONE, res') => res'
   641   | _ => error "Unfinished development at end of input")
   642   handle exn => error (exn_message exn);
   643 
   644 fun excursion trs = present_excursion (map (rpair no_pr) trs) ();
   645 
   646 end;
   647 
   648 
   649 (* toplevel program: independent of state *)
   650 
   651 fun program f =
   652   Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
   653 
   654 
   655 
   656 (** interactive transformations **)
   657 
   658 (* the global state reference *)
   659 
   660 val global_state = ref (toplevel, NONE: (exn * string) option);
   661 
   662 fun set_state state = global_state := (state, NONE);
   663 fun get_state () = fst (! global_state);
   664 fun exn () = snd (! global_state);
   665 
   666 
   667 (* the Isar source of transitions *)
   668 
   669 type 'a isar =
   670   (transition, (transition option,
   671     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
   672       Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
   673           Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
   674 
   675 
   676 (* apply transformers to global state *)
   677 
   678 nonfix >> >>>;
   679 
   680 fun >> tr =
   681   (case apply true tr (get_state ()) of
   682     NONE => false
   683   | SOME (state', exn_info) =>
   684       (global_state := (state', exn_info);
   685         print_exn exn_info;
   686         true));
   687 
   688 fun >>> [] = ()
   689   | >>> (tr :: trs) = if >> tr then >>> trs else ();
   690 
   691 (*Spurious interrupts ahead!  Race condition?*)
   692 fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
   693 
   694 fun raw_loop src =
   695   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
   696     NONE => (writeln "\nInterrupt."; raw_loop src)
   697   | SOME NONE => ()
   698   | SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ());
   699 
   700 fun loop src = ignore_interrupt raw_loop src;
   701 
   702 end;