Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
now allowing numeric identifiers to be used in 'file' annotations;
authorsultana
Tue, 03 Sep 2013 21:46:41 +0100
changeset 53391 b6fd2f441462
parent 53390 51b562922cb1
child 53392 a1a45fdc53a3
now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;
src/HOL/TPTP/TPTP_Parser/tptp_proof.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Sep 03 21:46:40 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Sep 03 21:46:41 2013 +0100
@@ -49,6 +49,8 @@
 
 open TPTP_Syntax
 
+exception ANNOT_STRUCTURE of general_term
+
 (*Extract name of inference rule, and the inferences it relies on*)
 (*This is tuned to work with LEO-II, and is brittle wrt upstream
   changes of the proof protocol.*)
@@ -119,6 +121,15 @@
               General_Data (Atomic_Word defname)])), _) =
                 (SOME (File (filename, defname)))
 
+      | analyse_annot
+         (General_Data
+           (Application
+             ("file",
+              [General_Data (Atomic_Word filename),
+               General_Data (Number (Int_num, defname))])), _) =
+                (SOME (File (filename, defname)))
+
+      | analyse_annot (other, _) = raise (ANNOT_STRUCTURE other)
   in
     case annot of
       NONE => NONE
isabelle