GrafiteAst.Quit (unused) removed.

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 03b67ade37c67d68ed63d4877aaaa7b12a1734ec..6731034318b266acdc4c9de000793276baf2445c 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -106,7 +106,6 @@ type 'term macro =
   (* real macros *)
   | Check of loc * 'term 
   | Hint of loc
-  | Quit of loc
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 55736e862e2cba8aa5ee548a823691af3f7810aa..d35a8af114936570f77f4be4366d655d04bd0b2b 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -182,7 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Quit _ -> "Quit"
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 4ced7a0afdd04e484836fc142195c70d2d597baa..76e5e6d86f13ae5257cd30e3a1e3081fecdf0eb9 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -326,4 +326,3 @@ let disambiguate_macro
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _ as macro ->
       metasenv,macro
-   | GrafiteAst.Quit _ -> assert false

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 834cbcf410f34b9f31379357057526ddceaf62d5..fadecd61e9e76825b355cfb2acdb541a436fd129 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -343,13 +343,7 @@ EXTEND
   ] ];
   
   macro: [
-    [ [ IDENT "quit"  ] -> GrafiteAst.Quit loc
-(*     | [ IDENT "abort" ] -> GrafiteAst.Abort loc *)
-(*     | [ IDENT "undo"   ]; steps = OPT NUMBER ->
-        GrafiteAst.Undo (loc, int_opt steps)
-    | [ IDENT "redo"   ]; steps = OPT NUMBER ->
-        GrafiteAst.Redo (loc, int_opt steps) *)
-    | [ IDENT "check"   ]; t = term ->
+    [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 

diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index 2dbd45c401d064d0fbaf6b3f2d8c0b232f4a7c47..4b88fa91dc6b2f5707b918abbf77acc75f95f5e3 100644 (file)
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -141,10 +141,8 @@
 
 
   <keyword-list _name = "Matita Macro" style = "Others 3" case-sensitive="TRUE">
-    <keyword>print</keyword>
     <keyword>check</keyword>
     <keyword>hint</keyword>
-    <keyword>quit</keyword>
     <keyword>set</keyword>
   </keyword-list>
   

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 91182d6ad44aa1aa0ed0dac991d101889eb82035..79c4fc4c57136cb884940ceae897768587613ae5 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -288,8 +288,6 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
       let t_and_ty = Cic.Cast (term,ty) in
       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
       [], parsed_text_length
-  (* TODO *)
-  | TA.Quit _ -> failwith "not implemented"
                                 
 and eval_executable include_paths (buffer : GText.buffer) guistuff
 lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt