Useless code removed.

diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml
index 02908dfd7303b56ec2986a273c5330f83e1f1d0a..19ac7da5c349121e25cec6ca33e8f18387c04dae 100644 (file)
--- 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 8f252a96795a10cc956d194bc7e707f6a38683b3..edb6b748b9dcfa57996320d038ce001b4608b616 100644 (file)
--- 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 eb39e019ddfc54472aa457d0eedb648adc8dd42c..680dec8e612850447ca1f179bb1e9a48dd6c19d3 100644 (file)
--- 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 e42f63ae22945f2c9e2dcd9c4033aa533478838b..2a17d938b9d74d0017776db845430ec5e1f5f73f 100644 (file)
--- 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 1f05a8837e1e5ecf95fe548839ade424960c73a6..6528eab9a9cbcb4d7446087dd7a02cd7aa538a75 100644 (file)
--- 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 5519e027ba102b5f96dad185e460780fdc48d7f2..add51ccf02eb6e88060fd848b5b79b1d42ef9794 100644 (file)
--- 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