From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jul 2006 12:19:25 +0000 (+0000)
Subject: GrafiteAst.Quit (unused) removed.
X-Git-Tag: make_still_working~7087
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5e24139bb91796541614daff84b99119dfb32caf;p=helm.git

GrafiteAst.Quit (unused) removed.
---

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 03b67ade3..673103431 100644
--- 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 55736e862..d35a8af11 100644
--- 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 4ced7a0af..76e5e6d86 100644
--- 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 834cbcf41..fadecd61e 100644
--- 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 2dbd45c40..4b88fa91d 100644
--- 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 91182d6ad..79c4fc4c5 100644
--- 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