# HG changeset patch # User wenzelm # Date 1231110769 -3600 # Node ID 28b0652aabd853550679d03f2f7eb2f20a8a175b # Parent b723fa577aa2d78a75c6b7054b64e2481acb4151 simplified tty model -- back to plain list history, which is independent of editor model; diff -r b723fa577aa2 -r 28b0652aabd8 src/Pure/Isar/isar.ML --- a/src/Pure/Isar/isar.ML Mon Jan 05 00:10:38 2009 +0100 +++ b/src/Pure/Isar/isar.ML Mon Jan 05 00:12:49 2009 +0100 @@ -6,15 +6,12 @@ signature ISAR = sig - type id = string - val no_id: id - val create_command: Toplevel.transition -> id - val init_point: unit -> unit + val init: unit -> unit + val exn: unit -> (exn * string) option val state: unit -> Toplevel.state val context: unit -> Proof.context val goal: unit -> thm val print: unit -> unit - val exn: unit -> (exn * string) option val >> : Toplevel.transition -> bool val >>> : Toplevel.transition list -> unit val linear_undo: int -> unit @@ -25,6 +22,10 @@ val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit val loop: unit -> unit val main: unit -> unit + + type id = string + val no_id: id + val create_command: Toplevel.transition -> id val insert_command: id -> id -> unit val remove_command: id -> unit end; @@ -33,6 +34,130 @@ struct +(** TTY model -- SINGLE-THREADED! **) + +(* the global state *) + +type history = (Toplevel.state * Toplevel.transition) list; + (*previous state, state transition -- regular commands only*) + +local + val global_history = ref ([]: history); + val global_state = ref Toplevel.toplevel; + val global_exn = ref (NONE: (exn * string) option); +in + +fun edit_history count f = NAMED_CRITICAL "Isar" (fn () => + let + fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE) + | edit n (st, hist) = edit (n - 1) (f st hist); + in edit count (! global_state, ! global_history) end); + +fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state); +fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state); + +fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn); +fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn); + +end; + + +fun init () = edit_history 1 (K (K (Toplevel.toplevel, []))); + +fun context () = Toplevel.context_of (state ()) + handle Toplevel.UNDEF => error "Unknown context"; + +fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ())))) + handle Toplevel.UNDEF => error "No goal present"; + +fun print () = Toplevel.print_state false (state ()); + + +(* history navigation *) + +local + +fun find_and_undo _ [] = error "Undo history exhausted" + | find_and_undo which ((prev, tr) :: hist) = + ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ()); + if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist); + +in + +fun linear_undo n = edit_history n (K (find_and_undo (K true))); + +fun undo n = edit_history n (fn st => fn hist => + find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist); + +fun kill () = edit_history 1 (fn st => fn hist => + find_and_undo + (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist); + +fun kill_proof () = edit_history 1 (fn st => fn hist => + if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist + else raise Toplevel.UNDEF); + +end; + + +(* interactive state transformations *) + +fun op >> tr = + (case Toplevel.transition true tr (state ()) of + NONE => false + | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true) + | SOME (st', NONE) => + let + val name = Toplevel.name_of tr; + val _ = if OuterKeyword.is_theory_begin name then init () else (); + val _ = + if OuterKeyword.is_regular name + then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else (); + in true end); + +fun op >>> [] = () + | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); + + +(* toplevel loop *) + +val crashes = ref ([]: exn list); + +local + +fun raw_loop secure src = + let + fun check_secure () = + (if secure then warning "Secure loop -- cannot exit to ML" else (); secure); + in + (case Source.get_single (Source.set_prompt Source.default_prompt src) of + NONE => if secure then quit () else () + | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) + handle exn => (Output.error_msg (Toplevel.exn_message exn) + handle crash => + (CRITICAL (fn () => change crashes (cons crash)); + warning "Recovering after Isar toplevel crash -- see also Isar.crashes"); + raw_loop secure src) + end; + +in + +fun toplevel_loop {init = do_init, welcome, sync, secure} = + (Context.set_thread_data NONE; + if do_init then init () else (); (* FIXME init editor model *) + if welcome then writeln (Session.welcome ()) else (); + uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ()); + +end; + +fun loop () = + toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; + +fun main () = + toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; + + + (** individual toplevel commands **) (* unique identification *) @@ -188,153 +313,6 @@ -(** TTY model -- single-threaded **) - -(* global point *) - -local val global_point = ref no_id in - -fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f); -fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point); - -end; - - -fun set_point id = change_point (K id); -fun init_point () = set_point no_id; - -fun point_state () = NAMED_CRITICAL "Isar" (fn () => - let val id = point () in (id, the_state id) end); - -fun state () = #2 (point_state ()); - -fun context () = - Toplevel.context_of (state ()) - handle Toplevel.UNDEF => error "Unknown context"; - -fun goal () = - #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ())))) - handle Toplevel.UNDEF => error "No goal present"; - -fun print () = Toplevel.print_state false (state ()); - - -(* global failure status *) - -local val global_exn = ref (NONE: (exn * string) option) in - -fun set_exn err = global_exn := err; -fun exn () = ! global_exn; - -end; - - -(* interactive state transformations *) - -fun op >> raw_tr = - let - val id = create_command raw_tr; - val {category, transition = tr, ...} = the_command id; - val (prev, prev_state) = point_state (); - val _ = - if is_regular category - then (dispose_commands (next_commands prev); change_commands (add_edge (prev, id))) - else (); - in - (case run true tr prev_state of - NONE => false - | SOME (status as Failed err) => (update_status status id; set_exn (SOME err); true) - | SOME status => - (update_status status id; set_exn NONE; - if is_regular category then set_point id else (); - true)) - end; - -fun op >>> [] = () - | op >>> (tr :: trs) = if op >> tr then op >>> trs else (); - - -(* implicit navigation wrt. proper commands *) - -local - -fun err_undo () = error "Undo history exhausted"; - -fun find_category which id = - (case #category (the_command id) of - Empty => err_undo () - | category => if which category then id else find_category which (prev_command id)); - -fun find_begin_theory id = - if id = no_id then err_undo () - else if is_some (Toplevel.init_of (#transition (the_command id))) then id - else find_begin_theory (prev_command id); - -fun undo_command id = - (case Toplevel.init_of (#transition (the_command id)) of - SOME name => prev_command id before ThyInfo.kill_thy name - | NONE => prev_command id); - -in - -fun linear_undo n = change_point (funpow n (fn id => undo_command (find_category is_proper id))); - -fun undo n = change_point (funpow n (fn id => undo_command - (find_category (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id))); - -fun kill () = change_point (fn id => undo_command - (if Toplevel.is_proof (the_state id) then find_category is_theory id else find_begin_theory id)); - -fun kill_proof () = change_point (fn id => - if Toplevel.is_proof (the_state id) then undo_command (find_category is_theory id) - else raise Toplevel.UNDEF); - -end; - - -(* toplevel loop *) - -val crashes = ref ([]: exn list); - -local - -fun raw_loop secure src = - let - fun check_secure () = - (if secure then warning "Secure loop -- cannot exit to ML" else (); secure); - val prev = point (); - val prev_name = Toplevel.name_of (#transition (the_command prev)); - val prompt_markup = - prev <> no_id ? Markup.markup - (Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt); - in - (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of - NONE => if secure then quit () else () - | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ()) - handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash => - (CRITICAL (fn () => change crashes (cons crash)); - warning "Recovering after Isar toplevel crash -- see also Isar.crashes"); - raw_loop secure src) - end; - -in - -fun toplevel_loop {init, welcome, sync, secure} = - (Context.set_thread_data NONE; - if init then (init_point (); init_commands ()) else (); - if welcome then writeln (Session.welcome ()) else (); - uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ()); - -end; - -fun loop () = - toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()}; - -fun main () = - toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()}; - - - (** editor model **) (* run commands *) @@ -375,7 +353,7 @@ local -structure P = struct open OuterParse open ValueParse end; +structure P = OuterParse; val op >> = Scan.>>; in