src/Pure/Isar/toplevel.ML
changeset 8465 df6549f5a01f
parent 7732 d62523296573
child 8561 2675e2f4dc61
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 15 18:30:45 2000 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 15 18:32:41 2000 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4    val interactive: bool -> transition -> transition
     1.5    val print: transition -> transition
     1.6    val reset: transition -> transition
     1.7 -  val init: (bool -> state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
     1.8 +  val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
     1.9    val exit: transition -> transition
    1.10    val kill: transition -> transition
    1.11    val keep: (state -> unit) -> transition -> transition
    1.12 @@ -93,22 +93,20 @@
    1.13  
    1.14  (* datatype state *)
    1.15  
    1.16 -datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) list;
    1.17 +datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option;
    1.18  
    1.19 -val toplevel = State [];
    1.20 +val toplevel = State None;
    1.21  
    1.22 -fun is_toplevel (State []) = true
    1.23 +fun is_toplevel (State None) = true
    1.24    | is_toplevel _ = false;
    1.25  
    1.26 -fun str_of_state (State []) = "at top level"
    1.27 -  | str_of_state (State ((node, _) :: _)) = str_of_node (History.current node);
    1.28 +fun str_of_state (State None) = "at top level"
    1.29 +  | str_of_state (State (Some (node, _))) = str_of_node (History.current node);
    1.30  
    1.31  
    1.32  (* prompt_state hook *)
    1.33  
    1.34 -fun prompt_state_default (State nodes) =
    1.35 -  let val len = length nodes
    1.36 -  in (if len < 2 then "" else string_of_int len) ^ Source.default_prompt end;
    1.37 +fun prompt_state_default (State _) = Source.default_prompt;
    1.38  
    1.39  val prompt_state_fn = ref prompt_state_default;
    1.40  fun prompt_state state = ! prompt_state_fn state;
    1.41 @@ -116,15 +114,15 @@
    1.42  
    1.43  (* print state *)
    1.44  
    1.45 -fun print_topnode _ (State []) = ()
    1.46 -  | print_topnode prt (State ((node, _) :: _)) = prt (History.current node);
    1.47 +fun print_current_node _ (State None) = ()
    1.48 +  | print_current_node prt (State (Some (node, _))) = prt (History.current node);
    1.49  
    1.50 -val print_state_context = print_topnode print_node_ctxt;
    1.51 +val print_state_context = print_current_node print_node_ctxt;
    1.52  
    1.53  fun print_state_default state =
    1.54    let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
    1.55      if begin_state = "" then () else writeln begin_state;
    1.56 -    print_topnode print_node state;
    1.57 +    print_current_node print_node state;
    1.58      if end_state = "" then () else writeln end_state
    1.59    end;
    1.60  
    1.61 @@ -136,8 +134,8 @@
    1.62  
    1.63  exception UNDEF;
    1.64  
    1.65 -fun node_history_of (State []) = raise UNDEF
    1.66 -  | node_history_of (State ((node, _) :: _)) = node;
    1.67 +fun node_history_of (State None) = raise UNDEF
    1.68 +  | node_history_of (State (Some (node, _))) = node;
    1.69  
    1.70  val node_of = History.current o node_history_of;
    1.71  
    1.72 @@ -186,10 +184,10 @@
    1.73  
    1.74  in
    1.75  
    1.76 -fun node_trans _ _ _ (State []) = raise UNDEF
    1.77 -  | node_trans int hist f (State ((node, term) :: nodes)) =
    1.78 +fun node_trans _ _ _ (State None) = raise UNDEF
    1.79 +  | node_trans int hist f (State (Some (node, term))) =
    1.80        let
    1.81 -        fun mk_state nd = State ((nd, term) :: nodes);
    1.82 +        fun mk_state nd = State (Some (nd, term));
    1.83  
    1.84          val cont_node = History.map (checkpoint_node int) node;
    1.85          val back_node = History.map (copy_node int) cont_node;
    1.86 @@ -221,9 +219,9 @@
    1.87  
    1.88  datatype trans =
    1.89    Reset |                                       (*empty toplevel*)
    1.90 -  Init of (bool -> state -> node) * ((node -> unit) * (node -> unit)) |
    1.91 -    (*push node; provide exit/kill operation*)
    1.92 -  Exit |                                        (*pop node*)
    1.93 +  Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
    1.94 +    (*init node; provide exit/kill operation*)
    1.95 +  Exit |                                        (*conclude node*)
    1.96    Kill |                                        (*abort node*)
    1.97    Keep of bool -> state -> unit |               (*peek at state*)
    1.98    History of node History.T -> node History.T | (*history operation (undo etc.)*)
    1.99 @@ -235,17 +233,18 @@
   1.100  local
   1.101  
   1.102  fun apply_tr _ Reset _ = toplevel
   1.103 -  | apply_tr int (Init (f, term)) (state as State nodes) =
   1.104 -      State ((History.init (undo_limit int) (f int state), term) :: nodes)
   1.105 -  | apply_tr _ Exit (State []) = raise UNDEF
   1.106 -  | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) =
   1.107 -      (exit (History.current node); State nodes)
   1.108 -  | apply_tr _ Kill (State []) = raise UNDEF
   1.109 -  | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) =
   1.110 -      (kill (History.current node); State nodes)
   1.111 +  | apply_tr int (Init (f, term)) (State None) =
   1.112 +      State (Some (History.init (undo_limit int) (f int), term))
   1.113 +  | apply_tr _ (Init _ ) (State (Some _)) = raise UNDEF
   1.114 +  | apply_tr _ Exit (State None) = raise UNDEF
   1.115 +  | apply_tr _ Exit (State (Some (node, (exit, _)))) =
   1.116 +      (exit (History.current node); State None)
   1.117 +  | apply_tr _ Kill (State None) = raise UNDEF
   1.118 +  | apply_tr _ Kill (State (Some (node, (_, kill)))) =
   1.119 +      (kill (History.current node); State None)
   1.120    | apply_tr int (Keep f) state = (exhibit_interrupt (f int) state; state)
   1.121 -  | apply_tr _ (History _) (State []) = raise UNDEF
   1.122 -  | apply_tr _ (History f) (State ((node, term) :: nodes)) = State ((f node, term) :: nodes)
   1.123 +  | apply_tr _ (History _) (State None) = raise UNDEF
   1.124 +  | apply_tr _ (History f) (State (Some (node, term))) = State (Some (f node, term))
   1.125    | apply_tr int (MapCurrent f) state = node_trans int false f state
   1.126    | apply_tr int (AppCurrent f) state = node_trans int true f state;
   1.127  
   1.128 @@ -327,7 +326,7 @@
   1.129  fun imperative f = keep (fn _ => f ());
   1.130  
   1.131  fun init_theory f exit kill =
   1.132 -  init (fn int => fn _ => Theory (f int))
   1.133 +  init (fn int => Theory (f int))
   1.134      (fn Theory thy => exit thy | _ => raise UNDEF)
   1.135      (fn Theory thy => kill thy | _ => raise UNDEF);
   1.136  
   1.137 @@ -419,9 +418,9 @@
   1.138  in
   1.139  
   1.140  fun excursion trs =
   1.141 -  (case excur trs (State []) of
   1.142 -    State [] => ()
   1.143 -  | _ => raise ERROR_MESSAGE "Open block(s) pending at end of input");
   1.144 +  (case excur trs (State None) of
   1.145 +    State None => ()
   1.146 +  | _ => raise ERROR_MESSAGE "Unfinished development at end of input");
   1.147  
   1.148  fun excursion_error trs =
   1.149    excursion trs handle exn => error (exn_message exn);