src/Pure/Isar/toplevel.ML
author wenzelm
Wed Jul 06 20:00:41 2005 +0200 (2005-07-06 ago)
changeset 16729 24c5c94aa967
parent 16682 154a84e1a4f7
child 16815 13d20ed9086c
permissions -rw-r--r--
debug: exception_trace;
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   datatype node = Theory of theory | Proof of ProofHistory.T | SkipProof of int History.T * theory
    11   type state
    12   val toplevel: state
    13   val is_toplevel: state -> bool
    14   val prompt_state_default: state -> string
    15   val prompt_state_fn: (state -> string) ref
    16   val print_state_context: state -> unit
    17   val print_state_default: bool -> state -> unit
    18   val print_state_fn: (bool -> state -> unit) ref
    19   val print_state: bool -> state -> unit
    20   val pretty_state: bool -> state -> Pretty.T list
    21   exception UNDEF
    22   val node_history_of: state -> node History.T
    23   val node_of: state -> node
    24   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    25   val theory_of: state -> theory
    26   val sign_of: state -> theory    (*obsolete*)
    27   val context_of: state -> Proof.context
    28   val proof_of: state -> Proof.state
    29   val enter_forward_proof: state -> Proof.state
    30   val quiet: bool ref
    31   val debug: bool ref
    32   val timing: bool ref
    33   val profiling: int ref
    34   exception TERMINATE
    35   exception RESTART
    36   type transition
    37   val undo_limit: bool -> int option
    38   val empty: transition
    39   val name_of: transition -> string
    40   val source_of: transition -> OuterLex.token list option
    41   val name: string -> transition -> transition
    42   val position: Position.T -> transition -> transition
    43   val source: OuterLex.token list -> transition -> transition
    44   val interactive: bool -> transition -> transition
    45   val print: transition -> transition
    46   val print': string -> transition -> transition
    47   val no_timing: transition -> transition
    48   val reset: transition -> transition
    49   val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
    50   val exit: transition -> transition
    51   val kill: transition -> transition
    52   val keep: (state -> unit) -> transition -> transition
    53   val keep': (bool -> state -> unit) -> transition -> transition
    54   val history: (node History.T -> node History.T) -> transition -> transition
    55   val imperative: (unit -> unit) -> transition -> transition
    56   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    57     -> transition -> transition
    58   val skip_proofs: bool ref
    59   val theory: (theory -> theory) -> transition -> transition
    60   val theory': (bool -> theory -> theory) -> transition -> transition
    61   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    62   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    63   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    64   val proof'': (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    65   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
    66   val proof_to_theory': (bool -> ProofHistory.T -> theory) -> transition -> transition
    67   val skip_proof: (int History.T -> int History.T) -> transition -> transition
    68   val skip_proof_to_theory: (int History.T -> bool) -> transition -> transition
    69   val unknown_theory: transition -> transition
    70   val unknown_proof: transition -> transition
    71   val unknown_context: transition -> transition
    72   val exn_message: exn -> string
    73   val apply: bool -> transition -> state -> (state * (exn * string) option) option
    74   val excursion_result: ((transition * (state -> state -> 'a -> 'a)) list * 'a) -> 'a
    75   val excursion: transition list -> unit
    76   val set_state: state -> unit
    77   val get_state: unit -> state
    78   val exn: unit -> (exn * string) option
    79   val >> : transition -> bool
    80   val >>> : transition list -> unit
    81   type 'a isar
    82   val loop: 'a isar -> unit
    83 end;
    84 
    85 structure Toplevel: TOPLEVEL =
    86 struct
    87 
    88 
    89 (** toplevel state **)
    90 
    91 (* datatype node *)
    92 
    93 datatype node =
    94   Theory of theory |
    95   Proof of ProofHistory.T |
    96   SkipProof of int History.T * theory;
    97 
    98 fun str_of_node (Theory _) = "in theory mode"
    99   | str_of_node _ = "in proof mode";
   100 
   101 fun pretty_context thy = [Pretty.block
   102   [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy),
   103     Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
   104 
   105 fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
   106 
   107 fun pretty_node_context (Theory thy) = pretty_context thy
   108   | pretty_node_context (Proof prf) = pretty_context (Proof.theory_of (ProofHistory.current prf))
   109   | pretty_node_context _ = [];
   110 
   111 fun pretty_node prf_only (Theory thy) = if prf_only then [] else pretty_context thy
   112   | pretty_node _ (Proof prf) = pretty_prf prf
   113   | pretty_node _ _ = [];
   114 
   115 
   116 (* datatype state *)
   117 
   118 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
   119 
   120 val toplevel = State NONE;
   121 
   122 fun is_toplevel (State NONE) = true
   123   | is_toplevel _ = false;
   124 
   125 fun str_of_state (State NONE) = "at top level"
   126   | str_of_state (State (SOME (node, _))) = str_of_node (History.current node);
   127 
   128 
   129 (* prompt_state hook *)
   130 
   131 fun prompt_state_default (State _) = Source.default_prompt;
   132 
   133 val prompt_state_fn = ref prompt_state_default;
   134 fun prompt_state state = ! prompt_state_fn state;
   135 
   136 
   137 (* print state *)
   138 
   139 fun pretty_current_node _ (State NONE) = []
   140   | pretty_current_node prt (State (SOME (node, _))) = prt (History.current node);
   141 
   142 val print_state_context =
   143   Pretty.writeln o Pretty.chunks o pretty_current_node pretty_node_context;
   144 
   145 fun pretty_state prf_only state =
   146   let val ref (begin_state, end_state, _) = Display.current_goals_markers in
   147     (case pretty_current_node (pretty_node prf_only) state of [] => []
   148     | prts =>
   149         (if begin_state = "" then [] else [Pretty.str begin_state]) @ prts @
   150         (if end_state = "" then [] else [Pretty.str end_state]))
   151   end;
   152 
   153 fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state);
   154 val print_state_fn = ref print_state_default;
   155 fun print_state state = ! print_state_fn state;
   156 
   157 
   158 (* top node *)
   159 
   160 exception UNDEF;
   161 
   162 fun node_history_of (State NONE) = raise UNDEF
   163   | node_history_of (State (SOME (node, _))) = node;
   164 
   165 val node_of = History.current o node_history_of;
   166 
   167 fun node_case f g state =
   168   (case node_of state of
   169     Theory thy => f thy
   170   | SkipProof (i, thy) => f thy
   171   | Proof prf => g (ProofHistory.current prf));
   172 
   173 val theory_of = node_case I Proof.theory_of;
   174 val sign_of = theory_of;
   175 val context_of = node_case ProofContext.init Proof.context_of;
   176 val proof_of = node_case (fn _ => raise UNDEF) I;
   177 
   178 val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
   179 
   180 
   181 
   182 (** toplevel transitions **)
   183 
   184 val quiet = ref false;
   185 val debug = ref false;
   186 val timing = Output.timing;
   187 val profiling = ref 0;
   188 
   189 exception TERMINATE;
   190 exception RESTART;
   191 exception EXCURSION_FAIL of exn * string;
   192 exception FAILURE of state * exn;
   193 
   194 
   195 (* recovery from stale theories *)
   196 
   197 (*note: proof commands should be non-destructive!*)
   198 
   199 local
   200 
   201 fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
   202 
   203 fun checkpoint_node true (Theory thy) = Theory (Theory.checkpoint thy)
   204   | checkpoint_node _ node = node;
   205 
   206 fun copy_node true (Theory thy) = Theory (Theory.copy thy)
   207   | copy_node _ node = node;
   208 
   209 val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!";
   210 
   211 fun return (result, NONE) = result
   212   | return (result, SOME exn) = raise FAILURE (result, exn);
   213 
   214 fun debug_trans f x =
   215   if ! debug then
   216     let val y = ref x in
   217       setmp Output.transform_exceptions false
   218         exception_trace (fn () => y := f x); ! y
   219     end
   220   else f x;
   221 
   222 fun interruptible f x =
   223   let val y = ref x
   224   in raise_interrupt (fn () => y := f x) (); ! y end;
   225 
   226 in
   227 
   228 fun node_trans _ _ _ (State NONE) = raise UNDEF
   229   | node_trans int hist f (State (SOME (node, term))) =
   230       let
   231         val cont_node = History.map (checkpoint_node int) node;
   232         val back_node = History.map (copy_node int) cont_node;
   233         fun state nd = State (SOME (nd, term));
   234         fun normal_state nd = (state nd, NONE);
   235         fun error_state nd exn = (state nd, SOME exn);
   236 
   237         val (result, err) =
   238           cont_node
   239           |> ((fn nd => f int nd)
   240               |> (if hist then History.apply_copy (copy_node int) else History.map)
   241               |> debug_trans
   242               |> interruptible
   243               |> transform_error)
   244           |> normal_state
   245           handle exn => error_state cont_node exn;
   246       in
   247         if is_stale result
   248         then return (error_state back_node (if_none err stale_theory))
   249         else return (result, err)
   250       end;
   251 
   252 end;
   253 
   254 
   255 (* primitive transitions *)
   256 
   257 (*Important note: recovery from stale theories is provided only for
   258   theory-level operations via MapCurrent and AppCurrent.  Other node
   259   or state operations should not touch theories at all.
   260 
   261   Also note that interrupts are enabled for Keep, MapCurrent, and
   262   AppCurrent only.*)
   263 
   264 datatype trans =
   265   Reset |                                       (*empty toplevel*)
   266   Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
   267     (*init node; provide exit/kill operation*)
   268   Exit |                                        (*conclude node*)
   269   Kill |                                        (*abort node*)
   270   Keep of bool -> state -> unit |               (*peek at state*)
   271   History of node History.T -> node History.T | (*history operation (undo etc.)*)
   272   MapCurrent of bool -> node -> node |          (*change node, bypassing history*)
   273   AppCurrent of bool -> node -> node;           (*change node, recording history*)
   274 
   275 fun undo_limit int = if int then NONE else SOME 0;
   276 
   277 local
   278 
   279 fun apply_tr _ Reset _ = toplevel
   280   | apply_tr int (Init (f, term)) (State NONE) =
   281       State (SOME (History.init (undo_limit int) (f int), term))
   282   | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF
   283   | apply_tr _ Exit (State NONE) = raise UNDEF
   284   | apply_tr _ Exit (State (SOME (node, (exit, _)))) =
   285       (exit (History.current node); State NONE)
   286   | apply_tr _ Kill (State NONE) = raise UNDEF
   287   | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
   288       (kill (History.current node); State NONE)
   289   | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state)
   290   | apply_tr _ (History _) (State NONE) = raise UNDEF
   291   | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
   292   | apply_tr int (MapCurrent f) state = node_trans int false f state
   293   | apply_tr int (AppCurrent f) state = node_trans int true f state;
   294 
   295 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   296   | apply_union int (tr :: trs) state =
   297       transform_error (apply_tr int tr) state
   298         handle UNDEF => apply_union int trs state
   299           | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
   300           | exn as FAILURE _ => raise exn
   301           | exn => raise FAILURE (state, exn);
   302 
   303 in
   304 
   305 fun apply_trans int trs state = (apply_union int trs state, NONE)
   306   handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
   307 
   308 end;
   309 
   310 
   311 (* datatype transition *)
   312 
   313 datatype transition = Transition of
   314  {name: string,
   315   pos: Position.T,
   316   source: OuterLex.token list option,
   317   int_only: bool,
   318   print: string list,
   319   no_timing: bool,
   320   trans: trans list};
   321 
   322 fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
   323   Transition {name = name, pos = pos, source = source,
   324     int_only = int_only, print = print, no_timing = no_timing, trans = trans};
   325 
   326 fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
   327   make_transition (f (name, pos, source, int_only, print, no_timing, trans));
   328 
   329 val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
   330 
   331 fun name_of (Transition {name, ...}) = name;
   332 fun source_of (Transition {source, ...}) = source;
   333 
   334 
   335 (* diagnostics *)
   336 
   337 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
   338 
   339 fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
   340 fun at_command tr = command_msg "At " tr ^ ".";
   341 
   342 fun type_error tr state =
   343   ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
   344 
   345 
   346 (* modify transitions *)
   347 
   348 fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
   349   (nm, pos, source, int_only, print, no_timing, trans));
   350 
   351 fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
   352   (name, pos, source, int_only, print, no_timing, trans));
   353 
   354 fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
   355   (name, pos, SOME src, int_only, print, no_timing, trans));
   356 
   357 fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
   358   (name, pos, source, int_only, print, no_timing, trans));
   359 
   360 fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   361   (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
   362 
   363 val print = print' "";
   364 
   365 val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
   366   (name, pos, source, int_only, print, true, trans));
   367 
   368 fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
   369   (name, pos, source, int_only, print, no_timing, trans @ [tr]));
   370 
   371 
   372 (* build transitions *)
   373 
   374 val reset = add_trans Reset;
   375 fun init f exit kill = add_trans (Init (f, (exit, kill)));
   376 val exit = add_trans Exit;
   377 val kill = add_trans Kill;
   378 val keep' = add_trans o Keep;
   379 val history = add_trans o History;
   380 val map_current = add_trans o MapCurrent;
   381 val app_current = add_trans o AppCurrent;
   382 
   383 fun keep f = add_trans (Keep (fn _ => f));
   384 fun imperative f = keep (fn _ => f ());
   385 
   386 fun init_theory f exit kill =
   387   init (fn int => Theory (f int))
   388     (fn Theory thy => exit thy | _ => raise UNDEF)
   389     (fn Theory thy => kill thy | _ => raise UNDEF);
   390 
   391 
   392 (* typed transitions *)
   393 
   394 (*The skip_proofs flag allows proof scripts to be skipped during
   395   interactive proof in order to speed up processing of large
   396   theories. While in skipping mode, states are represented as
   397   SkipProof (h, thy), where h contains a counter for the number of
   398   open proof blocks.*)
   399 
   400 val skip_proofs = ref false;
   401 
   402 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
   403 fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
   404 
   405 fun theory_to_proof f = app_current (fn int =>
   406   (fn Theory thy =>
   407         if ! skip_proofs then SkipProof (History.init (undo_limit int) 0,
   408           fst (SkipProof.global_skip_proof int (ProofHistory.current (f int thy))))
   409         else Proof (f int thy)
   410     | _ => raise UNDEF));
   411 
   412 fun proof''' b f = map_current (fn int => (fn Proof prf => Proof (f int prf)
   413   | SkipProof (h, thy) => if b then SkipProof (History.apply I h, thy) else raise UNDEF
   414   | _ => raise UNDEF));
   415 
   416 val proof' = proof''' true;
   417 val proof = proof' o K;
   418 val proof'' = proof''' false o K;
   419 
   420 fun proof_to_theory' f =
   421   map_current (fn int => (fn Proof prf => Theory (f int prf)
   422     | SkipProof (h, thy) => if History.current h = 0 then Theory thy else raise UNDEF
   423     | _ => raise UNDEF));
   424 
   425 val proof_to_theory = proof_to_theory' o K;
   426 
   427 fun skip_proof f = map_current (fn int =>
   428   (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF));
   429 
   430 fun skip_proof_to_theory p = map_current (fn int =>
   431   (fn SkipProof (h, thy) => if p h then Theory thy else raise UNDEF | _ => raise UNDEF));
   432 
   433 val unknown_theory = imperative (fn () => warning "Unknown theory context");
   434 val unknown_proof = imperative (fn () => warning "Unknown proof context");
   435 val unknown_context = imperative (fn () => warning "Unknown context");
   436 
   437 
   438 
   439 (** toplevel transactions **)
   440 
   441 (* print exceptions *)
   442 
   443 local
   444 
   445 fun with_context f xs =
   446   (case Context.get_context () of NONE => []
   447   | SOME thy => map (f thy) xs);
   448 
   449 fun raised name [] = "exception " ^ name ^ " raised"
   450   | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
   451   | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
   452 
   453 fun exn_msg _ TERMINATE = "Exit."
   454   | exn_msg _ RESTART = "Restart."
   455   | exn_msg _ Interrupt = "Interrupt."
   456   | exn_msg _ ERROR = "ERROR."
   457   | exn_msg _ (ERROR_MESSAGE msg) = msg
   458   | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   459   | exn_msg detailed (Context.DATA_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   460   | exn_msg detailed (Syntax.TRANSLATION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   461   | exn_msg false (THEORY (msg, _)) = msg
   462   | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
   463   | exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg
   464   | exn_msg _ (Proof.STATE (msg, _)) = msg
   465   | exn_msg _ (ProofHistory.FAIL msg) = msg
   466   | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
   467       fail_msg detailed "simproc" ((name, Position.none), exn)
   468   | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
   469   | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
   470   | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
   471   | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
   472   | exn_msg true (Syntax.AST (msg, asts)) =
   473       raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
   474   | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
   475   | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
   476         with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
   477   | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
   478   | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
   479   | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
   480   | exn_msg true (THM (msg, i, thms)) =
   481       raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
   482   | exn_msg _ Option = raised "Option" []
   483   | exn_msg _ UnequalLengths = raised "UnequalLengths" []
   484   | exn_msg _ Empty = raised "Empty" []
   485   | exn_msg _ Subscript = raised "Subscript" []
   486   | exn_msg _ (Fail msg) = raised "Fail" [msg]
   487   | exn_msg _ exn = General.exnMessage exn
   488 and fail_msg detailed kind ((name, pos), exn) =
   489   "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
   490 
   491 in
   492 
   493 fun exn_message exn = exn_msg (! debug) exn;
   494 
   495 fun print_exn NONE = ()
   496   | print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
   497 
   498 end;
   499 
   500 
   501 (* apply transitions *)
   502 
   503 val quiet = ref false;
   504 
   505 local
   506 
   507 fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =
   508   let
   509     val _ = conditional (not int andalso int_only) (fn () =>
   510       warning (command_msg "Interactive-only " tr));
   511 
   512     fun do_timing f x = (info (command_msg "" tr); timeap f x);
   513     fun do_profiling f x = profile (! profiling) f x;
   514 
   515     val (result, opt_exn) =
   516        state |> (apply_trans int trans
   517         |> (if ! profiling > 0 then do_profiling else I)
   518         |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
   519     val _ = conditional (int andalso not (! quiet) andalso
   520         exists (fn m => m mem_string print) ("" :: ! print_mode))
   521       (fn () => print_state false result);
   522   in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
   523 
   524 in
   525 
   526 fun apply int tr st =
   527   (case app int tr st of
   528     (_, SOME TERMINATE) => NONE
   529   | (_, SOME RESTART) => SOME (toplevel, NONE)
   530   | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info)
   531   | (state', SOME exn) => SOME (state', SOME (exn, at_command tr))
   532   | (state', NONE) => SOME (state', NONE));
   533 
   534 end;
   535 
   536 
   537 (* excursion: toplevel -- apply transformers -- toplevel *)
   538 
   539 local
   540 
   541 fun excur [] x = x
   542   | excur ((tr, f) :: trs) (st, res) =
   543       (case apply false tr st of
   544         SOME (st', NONE) =>
   545           excur trs (st', transform_error (fn () => f st st' res) () handle exn =>
   546             raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
   547       | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
   548       | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   549 
   550 in
   551 
   552 fun excursion_result (trs, res) =
   553   (case excur trs (State NONE, res) of
   554     (State NONE, res') => res'
   555   | _ => raise ERROR_MESSAGE "Unfinished development at end of input")
   556   handle exn => error (exn_message exn);
   557 
   558 fun excursion trs =
   559   excursion_result (map (fn tr => (tr, fn _ => fn _ => fn _ => ())) trs, ());
   560 
   561 end;
   562 
   563 
   564 
   565 (** interactive transformations **)
   566 
   567 (* the global state reference *)
   568 
   569 val global_state = ref (toplevel, NONE: (exn * string) option);
   570 
   571 fun set_state state = global_state := (state, NONE);
   572 fun get_state () = fst (! global_state);
   573 fun exn () = snd (! global_state);
   574 
   575 
   576 (* the Isar source of transitions *)
   577 
   578 type 'a isar =
   579   (transition, (transition option,
   580     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
   581       Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
   582           Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
   583 
   584 
   585 (* apply transformers to global state *)
   586 
   587 nonfix >> >>>;
   588 
   589 fun >> tr =
   590   (case apply true tr (get_state ()) of
   591     NONE => false
   592   | SOME (state', exn_info) =>
   593       (global_state := (state', exn_info);
   594         print_exn exn_info;
   595         true));
   596 
   597 fun >>> [] = ()
   598   | >>> (tr :: trs) = if >> tr then >>> trs else ();
   599 
   600 (*Note: this is for Poly/ML only, we really do not intend to exhibit
   601   interrupts here*)
   602 fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE;
   603 
   604 fun raw_loop src =
   605   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
   606     NONE => (writeln "\nInterrupt."; raw_loop src)
   607   | SOME NONE => ()
   608   | SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ());
   609 
   610 fun loop src = ignore_interrupt raw_loop src;
   611 
   612 end;