]> matita.cs.unibo.it Git - helm.git/commitdiff
Useless methods removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 18 Dec 2010 23:37:08 +0000 (23:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 18 Dec 2010 23:37:08 +0000 (23:37 +0000)
matita/matita/cicMathView.ml
matita/matita/cicMathView.mli

index 60d3b69cfab196d77c4057f989332e1dd2806350..43cedcec6b210c18e8c889bfab96f1d5833e9fe1 100644 (file)
@@ -40,11 +40,9 @@ object
   method update_font_size: unit
 
   method load_root : root:document_element -> unit
-  method action_toggle: document_element -> bool
   method remove_selections: unit
   method set_selection: document_element option -> unit
   method get_selections: document_element list
-  method has_selection: bool
 
     (** @raise Failure "no selection" *)
   method strings_of_selection: (MatitaGuiTypes.paste_kind * string) list
@@ -179,7 +177,6 @@ let text_width = 80 in
 object (self)
   inherit GSourceView2.source_view obj
 
-  method has_selection = (assert false : bool)
   method strings_of_selection = (assert false : (paste_kind * string) list)
   method update_font_size =
    self#misc#modify_font_by_name
@@ -566,8 +563,6 @@ IDIOTA: PRIMA SI FA LA LOCATE, POI LA PATTERN_OF. MEGLIO UN'UNICA pattern_of CHE
     | [] -> None
     | node :: _ -> Some (self#string_of_node ~paste_kind node)
 
-  method has_selection = self#get_selections <> []
-
     (** @return an associative list format -> string with all possible selection
      * formats. Rationale: in order to convert the selection to TERM or PATTERN
      * format we need the sequent, the metasenv, ... keeping all of them in a
index b3b97f7d0b2971293a3cde7886ac505b9e4fb445..260452bd5fed2d7a7f9d4215488c0faa86b569b5 100644 (file)
@@ -33,11 +33,9 @@ object
   method update_font_size: unit
 
   method load_root : root:document_element -> unit
-  method action_toggle: document_element -> bool
   method remove_selections: unit
   method set_selection: document_element option -> unit
   method get_selections: document_element list
-  method has_selection: bool
 
     (** @raise Failure "no selection" *)
   method strings_of_selection: (MatitaGuiTypes.paste_kind * string) list