# HG changeset patch
# User aspinall
# Date 1172921916 -3600
# Node ID 12892a6677c6ef644d48abdbe4bdd6745451d4d9
# Parent  a1cce5b241bec0492834bb07eab2cacb1713241a
Add Isabelle-specific objtypes

diff -r a1cce5b241be -r 12892a6677c6 src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Sat Mar 03 12:38:25 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Sat Mar 03 12:38:36 2007 +0100
@@ -12,6 +12,19 @@
     val accepted_inputs : (string * bool * (string list)) list 
 
     val location_of_position : Position.T -> PgipTypes.location
+
+    (* Additional types of objects in Isar scripts *)
+
+    val ObjTheoryBody : PgipTypes.objtype
+    val ObjTheoryDecl : PgipTypes.objtype
+    val ObjTheoryBodySubsection : PgipTypes.objtype
+    val ObjProofBody : PgipTypes.objtype
+    val ObjFormalComment : PgipTypes.objtype
+    val ObjClass : PgipTypes.objtype
+    val ObjTheoremSet : PgipTypes.objtype
+    val ObjOracle : PgipTypes.objtype
+    val ObjLocale : PgipTypes.objtype
+	
 end
 
 structure PgipIsabelle : PGIP_ISABELLE =
@@ -84,6 +97,28 @@
     in 
 	{ descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
     end 
+
+
+val [ObjTheoryBody,
+     ObjTheoryDecl,
+     ObjTheoryBodySubsection,
+     ObjProofBody,
+     ObjFormalComment,
+     ObjClass,
+     ObjTheoremSet,
+     ObjOracle,
+     ObjLocale] =
+    map PgipTypes.ObjOther 
+	["theory body", 
+	 "theory declaration",
+	 "theory subsection",
+	 "proof body",
+	 "formal comment",
+	 "class",
+	 "theorem set declaration",
+	 "oracle",
+	 "locale"];
+
 	
 end