src/Pure/Isar/toplevel.ML
changeset 25441 4028958d19ff
parent 25292 f082e59551b0
child 25527 330ca6e1dca8
equal deleted inserted replaced
25440:aa25d4d59383 25441:4028958d19ff
    55   val three_buffersN: string
    55   val three_buffersN: string
    56   val print3: transition -> transition
    56   val print3: transition -> transition
    57   val no_timing: transition -> transition
    57   val no_timing: transition -> transition
    58   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
    58   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) ->
    59     transition -> transition
    59     transition -> transition
    60   val init_empty: (unit -> unit) -> transition -> transition
    60   val init_empty: (state -> bool) -> (unit -> unit) -> transition -> transition
    61   val exit: transition -> transition
    61   val exit: transition -> transition
    62   val undo_exit: transition -> transition
    62   val undo_exit: transition -> transition
    63   val kill: transition -> transition
    63   val kill: transition -> transition
    64   val history: (node History.T -> node History.T) -> transition -> transition
    64   val history: (node History.T -> node History.T) -> transition -> transition
    65   val keep: (state -> unit) -> transition -> transition
    65   val keep: (state -> unit) -> transition -> transition
   387   Transaction.*)
   387   Transaction.*)
   388 
   388 
   389 datatype trans =
   389 datatype trans =
   390   Init of (bool -> theory) * ((theory -> unit) * (theory -> unit)) |
   390   Init of (bool -> theory) * ((theory -> unit) * (theory -> unit)) |
   391                                                     (*init node; with exit/kill operation*)
   391                                                     (*init node; with exit/kill operation*)
   392   InitEmpty of unit -> unit |                       (*init empty toplevel*)
   392   InitEmpty of (state -> bool) * (unit -> unit) |   (*init empty toplevel*)
   393   Exit |                                            (*conclude node -- deferred until init*)
   393   Exit |                                            (*conclude node -- deferred until init*)
   394   UndoExit |                                        (*continue after conclusion*)
   394   UndoExit |                                        (*continue after conclusion*)
   395   Kill |                                            (*abort node*)
   395   Kill |                                            (*abort node*)
   396   History of node History.T -> node History.T |     (*history operation (undo etc.)*)
   396   History of node History.T -> node History.T |     (*history operation (undo etc.)*)
   397   Keep of bool -> state -> unit |                   (*peek at state*)
   397   Keep of bool -> state -> unit |                   (*peek at state*)
   410 fun keep_state int f = controlled_execution (fn x => tap (f int) x);
   410 fun keep_state int f = controlled_execution (fn x => tap (f int) x);
   411 
   411 
   412 fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
   412 fun apply_tr int _ (Init (f, term)) (state as Toplevel _) =
   413       let val node = Theory (Context.Theory (f int), NONE)
   413       let val node = Theory (Context.Theory (f int), NONE)
   414       in safe_exit state; State (History.init (undo_limit int) node, term) end
   414       in safe_exit state; State (History.init (undo_limit int) node, term) end
   415   | apply_tr int _ (InitEmpty f) (state as Toplevel _) =
   415   | apply_tr int _ (InitEmpty (check, f)) (state as Toplevel _) =
   416       (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel)
   416       if check state then (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel)
       
   417       else raise UNDEF
   417   | apply_tr _ _ Exit (State (node, term)) =
   418   | apply_tr _ _ Exit (State (node, term)) =
   418       (the_global_theory (History.current node); Toplevel (SOME (node, term)))
   419       (the_global_theory (History.current node); Toplevel (SOME (node, term)))
   419   | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info
   420   | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info
   420   | apply_tr _ _ Kill (State (node, (_, kill))) =
   421   | apply_tr _ _ Kill (State (node, (_, kill))) =
   421       (kill (the_global_theory (History.current node)); toplevel)
   422       (kill (the_global_theory (History.current node)); toplevel)
   506 
   507 
   507 
   508 
   508 (* basic transitions *)
   509 (* basic transitions *)
   509 
   510 
   510 fun init_theory f exit kill = add_trans (Init (f, (exit, kill)));
   511 fun init_theory f exit kill = add_trans (Init (f, (exit, kill)));
   511 val init_empty = add_trans o InitEmpty;
   512 fun init_empty check f = add_trans (InitEmpty (check, f));
   512 val exit = add_trans Exit;
   513 val exit = add_trans Exit;
   513 val undo_exit = add_trans UndoExit;
   514 val undo_exit = add_trans UndoExit;
   514 val kill = add_trans Kill;
   515 val kill = add_trans Kill;
   515 val history = add_trans o History;
   516 val history = add_trans o History;
   516 val keep' = add_trans o Keep;
   517 val keep' = add_trans o Keep;
   739         true));
   740         true));
   740 
   741 
   741 fun >>> [] = ()
   742 fun >>> [] = ()
   742   | >>> (tr :: trs) = if >> tr then >>> trs else ();
   743   | >>> (tr :: trs) = if >> tr then >>> trs else ();
   743 
   744 
   744 fun init_state () = (>> (init_empty (K ()) empty); ());
   745 fun init_state () = (>> (init_empty (K true) (K ()) empty); ());
   745 
   746 
   746 
   747 
   747 (* the Isar source of transitions *)
   748 (* the Isar source of transitions *)
   748 
   749 
   749 type 'a isar =
   750 type 'a isar =