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