From 6ab0b3e34eee7c4efa628e2994b461347d1bcebf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Dec 2010 17:01:01 +0000 Subject: [PATCH] Useless code removed. --- matita/matita/cicMathView.ml | 2 +- matita/matita/cicMathView.mli | 4 ++-- matita/matita/matitaGui.ml | 8 ++----- matita/matita/matitaMathView.ml | 4 +--- matita/matita/matitaScript.ml | 38 +++++++++++---------------------- matita/matita/matitaScript.mli | 7 ------ 6 files changed, 18 insertions(+), 45 deletions(-) diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index 02908dfd7..19ac7da5c 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -30,7 +30,7 @@ open MatitaGtkMisc open MatitaGuiTypes open GtkSourceView2 -let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >));; +let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status >));; let register_matita_script_current f = matita_script_current := f;; let get_matita_script_current () = !matita_script_current ();; diff --git a/matita/matita/cicMathView.mli b/matita/matita/cicMathView.mli index 8f252a967..edb6b748b 100644 --- a/matita/matita/cicMathView.mli +++ b/matita/matita/cicMathView.mli @@ -63,5 +63,5 @@ val screenshot: (* CSC: these functions should completely disappear; bad design; the object type is MatitaScript.script *) -val register_matita_script_current: (unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >) -> unit -val get_matita_script_current: unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit > +val register_matita_script_current: (unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status >) -> unit +val get_matita_script_current: unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status > diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index eb39e019d..680dec8e6 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -1005,15 +1005,11 @@ class gui () = `ProofMode -> sequents_viewer#nload_sequents grafite_status; (try - script#setGoal - (Some (Continuationals.Stack.find_goal grafite_status#stack)); let goal = - match script#goal with - None -> assert false - | Some n -> n + Continuationals.Stack.find_goal grafite_status#stack in sequents_viewer#goto_sequent grafite_status goal - with Failure _ -> script#setGoal None); + with Failure _ -> ()); | `CommandMode -> sequents_viewer#load_logo in script#addObserver sequents_observer; diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index e42f63ae2..2a17d938b 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -105,8 +105,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- `Old []; - self#script#setGoal None + _metasenv <- `Old [] method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit = fun (status : #GrafiteTypes.status) -> @@ -185,7 +184,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = let goal_switch = try List.assoc page page2goal with Not_found -> assert false in - self#script#setGoal (Some (goal_of_switch goal_switch)); self#render_page status ~page ~goal_switch)) method private render_page: diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 1f05a8837..6528eab9a 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -70,8 +70,7 @@ type guistuff = { ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } -let eval_with_engine include_paths guistuff grafite_status user_goal - skipped_txt nonskipped_txt st +let eval_with_engine include_paths guistuff grafite_status skipped_txt nonskipped_txt st = let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt @@ -100,7 +99,7 @@ let eval_with_engine include_paths guistuff grafite_status user_goal let pp_eager_statement_ast = GrafiteAstPp.pp_statement -let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = +let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in match mac with | TA.Screenshot (_,name) -> @@ -168,25 +167,24 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us | TA.NAutoInteractive (_, (Some _,_)) -> assert false let rec eval_executable include_paths (buffer : GText.buffer) guistuff -grafite_status user_goal unparsed_text skipped_txt nonskipped_txt -script ex loc +grafite_status unparsed_text skipped_txt nonskipped_txt script ex loc = try ignore (buffer#move_mark (`NAME "beginning_of_statement") ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars (Glib.Utf8.length skipped_txt))) ; eval_with_engine include_paths - guistuff grafite_status user_goal skipped_txt nonskipped_txt + guistuff grafite_status skipped_txt nonskipped_txt (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], "", 0 | GrafiteEngine.NMacro (_loc,macro) -> eval_nmacro include_paths buffer guistuff grafite_status - user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro + unparsed_text (skipped_txt ^ nonskipped_txt) script macro and eval_statement include_paths (buffer : GText.buffer) guistuff - grafite_status user_goal script statement + grafite_status script statement = let st,unparsed_text = match statement with @@ -212,12 +210,12 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff | GrafiteAst.Executable (loc, ex) -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in eval_executable include_paths buffer guistuff - grafite_status user_goal unparsed_text skipped nonskipped script ex loc + grafite_status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)) when Helm_registry.get_bool "matita.execcomments" -> let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in eval_executable include_paths buffer guistuff - grafite_status user_goal unparsed_text skipped nonskipped script ex loc + grafite_status unparsed_text skipped nonskipped script ex loc | GrafiteAst.Comment (loc, _) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in @@ -225,7 +223,7 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff let s,text,len = try eval_statement include_paths buffer guistuff - grafite_status user_goal script (`Raw s) + grafite_status script (`Raw s) with HExtlib.Localized (floc, exn) -> HExtlib.raise_localized_exception @@ -455,9 +453,6 @@ object (self) * the script. * Invariant: this list length is 1 + length of statements *) - (** goal as seen by the user (i.e. metano corresponding to current tab) *) - val mutable userGoal = (None : int option) - (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter @@ -693,7 +688,7 @@ object (self) let entries, newtext, parsed_len = try eval_statement self#include_paths buffer guistuff - self#grafite_status userGoal self (`Raw s) + self#grafite_status self (`Raw s) with End_of_file -> raise Margin in let time2 = Unix.gettimeofday () in @@ -717,10 +712,7 @@ object (self) end; end; self#moveMark (Glib.Utf8.length new_text); - buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext; - (* here we need to set the Goal in case we are going to cursor (or to - bottom) and we will face a macro *) - userGoal <- None + buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext method private _retract offset grafite_status new_statements new_history = NCicLibrary.time_travel grafite_status; @@ -884,7 +876,6 @@ object (self) method private reset_buffer = statements <- []; history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ]; - userGoal <- None; self#notify; buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter @@ -985,11 +976,6 @@ object (self) with Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" - method stack = (assert false : Continuationals.Stack.t) (* MATITA 1.0 GrafiteTypes.get_stack - self#grafite_status *) - method setGoal n = userGoal <- n - method goal = userGoal - method bos = match history with | _::[] -> true @@ -1053,5 +1039,5 @@ let current () = let iter_scripts f = List.iter f !_script;; let _ = - CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >) + CicMathView.register_matita_script_current (current :> unit -> < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status >) ;; diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 5519e027b..add51ccf0 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -84,13 +84,6 @@ object method loadFromFile : string -> unit method saveToFile : unit -> unit - (** {2 Current proof} (if any) *) - - method stack: Continuationals.Stack.t (** @raise Statement_error *) - - method setGoal: int option -> unit - method goal: int option - (** end of script, true if the whole script has been executed *) method eos: bool method bos: bool -- 2.39.2