no message

MOF.sml

@@ -0,0 +1,71 @@
+structure MOF : sig
+  type 'a equal
+  type num
+  type 'a rexp
+  type char
+  type attribute_types
+  type class_hierarchy
+  val mt : class_hierarchy
+  val classes : class_hierarchy -> string list
+  val all_entities :
+    class_hierarchy -> ((string * (string * string) rexp) list) list
+  val all_attributes : class_hierarchy -> ((string * attribute_types) list) list
+  val remove_overrides : 'b equal -> ('a -> 'b) -> 'a list -> 'a list
+end = struct
+
+type 'a equal = {equal : 'a -> 'a -> bool};
+val equal = #equal : 'a equal -> 'a -> 'a -> bool;
+
+datatype int = Int_of_integer of IntInf.int;
+
+datatype num = One | Bit0 of num | Bit1 of num;
+
+datatype 'a rexp = Empty | Atom of 'a | Alt of 'a rexp * 'a rexp |
+  Conc of 'a rexp * 'a rexp | Star of 'a rexp;
+
+datatype char = Zero_char | Char of num;
+
+datatype attribute_types = File_T of string | Image_file_T of string |
+  Thms_T of string list | Int_T of int | Bool_T of bool | String_T of string |
+  Text_T of string | Range_T of int * int option | Enum_T of string list;
+
+datatype class_hierarchy =
+  Class_T of
+    string * class_hierarchy list * (string * attribute_types) list *
+      (string * (string * string) rexp) list;
+
+fun eq A_ a b = equal A_ a b;
+
+fun maps f [] = []
+  | maps f (x :: xs) = f x @ maps f xs;
+
+fun implode _ = raise Fail "String.implode";
+
+val mt : class_hierarchy =
+  Class_T (implode [Char (Bit1 (Bit1 (Bit1 (Bit1 (Bit0 One)))))], [], [], []);
+
+fun member A_ [] y = false
+  | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y;
+
+fun map f [] = []
+  | map f (x21 :: x22) = f x21 :: map f x22;
+
+fun classes (Class_T (name, sub_classes, attr, comps)) =
+  name :: maps classes sub_classes;
+
+fun entities (Class_T (x1, x2, x3, x4)) = x4;
+
+fun all_entities (Class_T (name, sub_classes, attr, comps)) =
+  comps :: map entities sub_classes;
+
+fun attributes (Class_T (x1, x2, x3, x4)) = x3;
+
+fun all_attributes (Class_T (name, sub_classes, attr, comps)) =
+  attr :: map attributes sub_classes;
+
+fun remove_overrides B_ f [] = []
+  | remove_overrides B_ f (a :: r) =
+    (if member B_ (map f r) (f a) then remove_overrides B_ f r
+      else a :: remove_overrides B_ f r);
+
+end; (*struct MOF*)

examples/simple/Example.thy

@@ -0,0 +1,154 @@
+theory Example
+  imports  "../../ontologies/CENELEC_50126"
+  keywords "Term" :: diag 
+begin
+
+section{* Some show-off's of general antiquotations. *}
+
+  
+(* some show-off of standard anti-quotations: *) 
+print_attributes
+print_antiquotations
+
+text{*  @{thm refl}  of name @{thm [source] refl} 
+        @{thm[mode=Rule] conjI}
+        @{file "../../Isa_DOF.thy"} 
+        @{value "3+4::int"} 
+        @{const hd} 
+        @{theory List}}
+        @{term "3"} 
+        @{type bool}  
+        @{term [show_types] "f x = a + x"} *}
+   
+
+section{* Example *}
+
+text*[ass1::assumption] {* Brexit means Brexit *}
+
+text*[hyp1::hypothesis] {* P means not P *}
+  
+  
+text*[ass122::srac] {* The overall sampling frequence of the odometer
+subsystem is therefore 14 khz, which includes sampling, computing and
+result communication times... *}
+  
+text*[t10::test_result] {* This is a meta-test. This could be an ML-command
+that governs the external test-execution via, eg., a makefile or specific calls
+to a test-environment or test-engine *}
+
+
+text \<open> As established by @{docref (unchecked) \<open>t10\<close>}, 
+                         @{docref (define) \<open>t10\<close>}
+       the               @{docref  \<open>t10\<close>}
+       the               @{docref \<open>ass122\<close>}
+     \<close>  
+text \<open> safety related applicability condition @{srac \<open>ass122\<close>}.
+       exported constraint @{ec \<open>ass122\<close>}.       
+     \<close>
+  
+text{*
+   And some ontologically inconsistent reference:
+    @{hypothesis \<open>ass1\<close>} as well as 
+    
+*} 
+-- "very wrong"
+
+text{*
+   And some ontologically inconsistent reference:
+    @{assumption \<open>hyp1\<close>} as well as 
+    
+*} 
+-- "very wrong"
+
+  
+  
+text{*
+   And some ontologically inconsistent reference:
+    @{test_result \<open>ass122\<close>} as well as 
+    
+*} 
+-- wrong  
+  
+text{*
+   And some other ontologically inconsistent reference:
+    @{ec \<open>t10\<close>} as well as  
+*} 
+-- wrong  
+  
+  
+
+section{* Some Tests for Ontology Framework and its CENELEC Instance *}  
+
+declare_reference [lalala::requirement, alpha="main", beta=42]
+
+declare_reference [lalala::quod] (* shouldn't work *)
+
+declare_reference [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
+  
+paragraph*[sdf]{* just a paragraph *}  
+paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>  
+
+subsection*[sdf]{* shouldn't work, multiple ref. *}  
+
+section*[sedf::requirement, alpja= refl]{* works again. One can hover over the class constraint and 
+                              jump to its definition. *}  
+text\<open>\label{sedf}\<close>  (* Hack to make the LaTeX-ing running. Should disappear. *)
+  
+section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting,
+but wrong doc_class constraint. *}  
+
+section{* Text Antiquotation Infrastructure ... *}  
+                  
+text{* @{docref \<open>lalala\<close>} -- produces warning. *}  
+text{* @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. *}  
+
+text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
+
+text{* @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
+                         Note that the link is actually a srac, which, according to 
+                         the ontology, happens to be an "ec".  *}
+
+text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". *}
+
+
+
+text{* Here is a reference to @{docref \<open>sedf\<close>} *}    
+(* works currently only in connection with the above label-hack. 
+   Try to hover over the sedf - link and activate it !!! *)
+ 
+
+
+
+
+
+
+
+
+
+
+
+  
+section{* A Small Example for a Command Definition --- just to see how this works in principle. *}
+
+ML{* 
+val opt_modes =
+  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
+
+val _ =
+  Outer_Syntax.command @{command_keyword Term} "read and print term"
+    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
+
+*}
+
+lemma "True" by simp
+  
+Term "a + b = b + a"
+
+term "a + b = b + a"  
+  
+section(in order){* sdfsdf*}  (* undocumented trouvaille when analysing the code *) 
+
+  
+end
+  
+    

examples/simple/IdirExample.thy

@@ -0,0 +1,9 @@
+theory IdirExample
+  imports  "../../ontologies/ScientificPaperOnto"
+
+begin
+
+text*[p1::Paragraph] {* ceci est un paragraphe *}
+text*[abs::Abstract, content = p1]{* *}
+
+end

ontologies/ScientificPaperOnto.thy

@@ -0,0 +1,26 @@
+theory ScientificPaperOnto
+  imports "../Isa_DOF"
+
+begin
+
+doc_class Paragraph = 
+    content :: "string list" 
+
+doc_class Abstract =
+     content ::  Paragraph 
+
+doc_class SubSection =
+    id :: integer
+    content :: "Paragraph list"
+
+doc_class Section =
+    id :: integer
+    content :: "Paragraph list"
+    itsSubSection :: "SubSection list"
+
+doc_class Article = 
+    content :: "(Abstract + Section) list"
+    where
+    "(Abstract.
+      Section*)"
+end