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