# HG changeset patch
# User wenzelm
# Date 1331846407 -3600
# Node ID 4e032ac36134633319d25e533e0b6f71510704e2
# Parent  d0181abdbdac82469a6ee1ebd7ecf9314b93d7e4
more precise TPTP keywords and dependencies;

diff -r d0181abdbdac -r 4e032ac36134 Admin/update-keywords
--- a/Admin/update-keywords	Thu Mar 15 22:08:53 2012 +0100
+++ b/Admin/update-keywords	Thu Mar 15 22:20:07 2012 +0100
@@ -13,7 +13,7 @@
 isabelle keywords \
   "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
   "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
-  "$LOG/HOL-SPARK.gz"
+  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz"
 
 isabelle keywords -k ZF \
   "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
diff -r d0181abdbdac -r 4e032ac36134 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Mar 15 22:08:53 2012 +0100
+++ b/etc/isar-keywords.el	Thu Mar 15 22:20:07 2012 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -108,6 +108,7 @@
     "hide_const"
     "hide_fact"
     "hide_type"
+    "import_tptp"
     "inductive"
     "inductive_cases"
     "inductive_set"
@@ -484,6 +485,7 @@
     "hide_const"
     "hide_fact"
     "hide_type"
+    "import_tptp"
     "inductive"
     "inductive_set"
     "instantiation"
diff -r d0181abdbdac -r 4e032ac36134 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Mar 15 22:08:53 2012 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 15 22:20:07 2012 +0100
@@ -1232,14 +1232,21 @@
 
 HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz
 
-$(LOG)/HOL-TPTP.gz: \
-  $(OUT)/HOL \
+$(LOG)/HOL-TPTP.gz: $(OUT)/HOL \
+  TPTP/ATP_Problem_Import.thy \
+  TPTP/ATP_Theory_Export.thy \
+  TPTP/CASC_Setup.thy \
   TPTP/ROOT.ML \
+  TPTP/TPTP_Parser.thy \
+  TPTP/TPTP_Parser/ml_yacc_lib.ML \
+  TPTP/TPTP_Parser/tptp_interpret.ML \
+  TPTP/TPTP_Parser/tptp_lexyacc.ML \
+  TPTP/TPTP_Parser/tptp_parser.ML \
+  TPTP/TPTP_Parser/tptp_problem_name.ML \
+  TPTP/TPTP_Parser/tptp_syntax.ML \
+  TPTP/TPTP_Parser_Test.thy \
   TPTP/atp_problem_import.ML \
-  TPTP/ATP_Problem_Import.thy \
-  TPTP/atp_theory_export.ML \
-  TPTP/ATP_Theory_Export.thy \
-  TPTP/CASC_Setup.thy
+  TPTP/atp_theory_export.ML
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
 
 
diff -r d0181abdbdac -r 4e032ac36134 src/HOL/TPTP/TPTP_Parser.thy
--- a/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 22:08:53 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 22:20:07 2012 +0100
@@ -9,7 +9,7 @@
 
 theory TPTP_Parser
 imports Main
-keywords "import_tptp" :: diag (* FIXME !? *) 
+keywords "import_tptp" :: thy_decl 
 uses
   "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
 
diff -r d0181abdbdac -r 4e032ac36134 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Mar 15 22:08:53 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Mar 15 22:20:07 2012 +0100
@@ -887,14 +887,9 @@
   in TPTP_Data.map (cons ((prob_name, result))) thy' end
 
 val _ =
-  Outer_Syntax.improper_command "import_tptp" "import TPTP problem"
-   Keyword.diag (*FIXME why diag?*)
-   (Parse.string >>
-    (fn file_name =>
-      Toplevel.theory (fn thy =>
-        import_file true (Path.explode file_name |> Path.dir)
-         (Path.explode file_name) [] [] thy
-        )))
+  Outer_Syntax.improper_command "import_tptp" "import TPTP problem" Keyword.thy_decl
+    (Parse.path >> (fn path =>
+      Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
 
 
 (*Used for debugging. Returns all files contained within a directory or its