Added global command: check_doc_global

(* checking unresolved forward references for the moment *)

Isa_DOF.thy

@@ -22,10 +22,10 @@ theory Isa_DOF                (* Isabelle Document Ontology Framework *)
            
   keywords "+=" ":=" "accepts" "rejects"
 
-  and      "title*"      "subtitle*"
-           "chapter*" "section*"    "subsection*"   "subsubsection*" 
-           "text*"       
+  and      "title*"     "subtitle*"
+           "chapter*"  "section*"    "subsection*"   "subsubsection*" 
            "paragraph*"  "subparagraph*" 
+           "text*"       
            "figure*"
            "side_by_side_figure*" 
            :: document_body
@@ -35,7 +35,7 @@ theory Isa_DOF                (* Isabelle Document Ontology Framework *)
 
   and      "lemma*" "theorem*" "assert*"  ::thy_decl
 
-  and      "print_doc_classes" "print_doc_items" "gen_sty_template" :: diag
+  and      "print_doc_classes" "print_doc_items" "gen_sty_template"  "check_doc_global" :: diag
            
   
 begin
@@ -563,6 +563,14 @@ fun print_doc_classes b ctxt =
         writeln "=====================================\n\n\n" 
     end;
 
+fun check_doc_global (strict_checking : bool) ctxt = 
+    let val {docobj_tab={tab = x, ...}, ...} = get_data ctxt;
+        val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x)
+    in if null S 
+       then () 
+       else error("Global consistency error - Unresolved forward references: "^ String.concatWith "," S)   
+    end 
+
 val _ =
   Outer_Syntax.command @{command_keyword print_doc_classes}
     "print document classes"
@@ -575,6 +583,13 @@ val _ =
     (Parse.opt_bang >> (fn b =>
       Toplevel.keep (print_doc_items b o Toplevel.context_of)));
 
+val _ =
+  Outer_Syntax.command @{command_keyword check_doc_global}
+    "check global document consistency"
+    (Parse.opt_bang >> (fn b =>
+      Toplevel.keep (check_doc_global b o Toplevel.context_of)));
+
+
 fun toStringLaTeXNewKeyCommand env long_name =
     "\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n" 
 

examples/simple/Concept_Example.thy

@@ -44,7 +44,7 @@ ML\<open>@{trace_attribute struct}\<close>
 print_doc_classes
 print_doc_items
 
-
+check_doc_global
 
 end 
   

ontologies/Conceptual.thy

@@ -6,14 +6,14 @@ doc_class A =
    x :: int  
 
 doc_class B =
-   x :: "string"               (* attributes live in their own name-space *)
-   y :: "string list"          <= "[]"  (* and can have arbitrary type constructors *)
-                                        (* LaTeX may have problems with this, though *)
-
-doc_class C = B +
-   z :: "A option"             <= None  (* A LINK, i.e. an attribute that has a type
-                                           referring to a document class. Mathematical
-                                           relations over document items can be modeled. *)
+   x :: "string"                            (* attributes live in their own name-space *)
+   y :: "string list"          <= "[]"      (* and can have arbitrary type constructors *)
+                                            (* LaTeX may have problems with this, though *)
+                                            
+doc_class C = B +                           
+   z :: "A option"             <= None      (* A LINK, i.e. an attribute that has a type
+                                               referring to a document class. Mathematical
+                                               relations over document items can be modeled. *)
    g :: "thm"
 
 datatype enum = X1 | X2 | X3
@@ -26,15 +26,15 @@ doc_class D = B +
    a2 :: int                   <= 0
 
 doc_class E = D +
-   x :: "string"              <= "''qed''" (* overriding default *)
+   x :: "string"              <= "''qed''"  (* overriding default *)
    
 doc_class F  = 
    r :: "thm list"
    u :: "file"
    s :: "typ list"
-   b :: "(A \<times> C) set"         <= "{}"        (* This is a relation link, roughly corresponding
-                                                 to an association class. It can be used to track
-                                                 claims to result - relations, for example.*) 
+   b :: "(A \<times> C) set"         <= "{}"       (* This is a relation link, roughly corresponding
+                                                to an association class. It can be used to track
+                                                claims to result - relations, for example.*) 
 doc_class G = C +                                               
    g :: "thm"  <= "@{thm ''HOL.refl''}"
 

test/cenelec/Example.thy

@@ -99,6 +99,7 @@ text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologi
 text{* Here is a reference to @{docref \<open>sedf\<close>} *}    
 (* shouldn't work: label exists, but definition was finally rejected to to errors. *)
  
+check_doc_global (* shoudn't work : Unresolved forward references: lalala,blablabla *)
 
 section \<open>Miscellaneous\<close> 
   

test/conceptual/Attributes.thy

@@ -114,4 +114,6 @@ ML\<open>@{trace_attribute figs1}\<close>
 
 print_doc_items
 
+check_doc_global
+
 end