From 7bac8af3711810b6d6ade5134eda2f62bf6b0ba3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Jul 2006 12:19:25 +0000
Subject: [PATCH] GrafiteAst.Quit (unused) removed.

---
 components/grafite/grafiteAst.ml                 | 1 -
 components/grafite/grafiteAstPp.ml               | 1 -
 components/grafite_parser/grafiteDisambiguate.ml | 1 -
 components/grafite_parser/grafiteParser.ml       | 8 +-------
 matita/matita.lang                               | 2 --
 matita/matitaScript.ml                           | 2 --
 6 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 03b67ade3..673103431 100644
--- a/components/grafite/grafiteAst.ml
+++ b/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/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 55736e862..d35a8af11 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/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/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 4ced7a0af..76e5e6d86 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/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/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 834cbcf41..fadecd61e 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/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/matita/matita.lang b/matita/matita.lang
index 2dbd45c40..4b88fa91d 100644
--- a/matita/matita.lang
+++ b/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/matita/matitaScript.ml b/matita/matitaScript.ml
index 91182d6ad..79c4fc4c5 100644
--- a/matita/matitaScript.ml
+++ b/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
-- 
2.39.2