diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 51824d8..f9ff3ac 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -38,6 +38,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) and "open_monitor*" "close_monitor*" "declare_reference*" "update_instance*" "doc_class" + "onto_class" (* a wish from Idir *) "define_shortcut*" "define_macro*" :: thy_decl and "text*" "text-macro*" :: document_body @@ -124,9 +125,11 @@ fun map_snd f (x,y) = (x,f y) \ section\ A HomeGrown Document Type Management (the ''Model'') \ - + + ML\ structure DOF_core = + struct type docclass_struct = {params : (string * sort) list, (*currently not used *) @@ -1932,11 +1935,14 @@ fun add_doc_class_cmd overloaded (raw_params, binding) |> ISA_core.declare_ISA_class_accessor_and_check_instance binding end; + +(* repackaging argument list *) +fun add_doc_class_cmd' (((overloaded, hdr), (parent, attrs)),((rejects,accept_rex),invars)) = + (add_doc_class_cmd {overloaded = overloaded} hdr parent attrs rejects accept_rex invars) + val parse_invariants = Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term) -val _ = - Outer_Syntax.command \<^command_keyword>\doc_class\ "define document class" - ((Parse_Spec.overloaded +val parse_doc_class = (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) -- (\<^keyword>\=\ |-- Scan.option (Parse.typ --| \<^keyword>\+\) @@ -1945,10 +1951,22 @@ val _ = -- ( Scan.optional (\<^keyword>\rejects\ |-- Parse.enum1 "," Parse.term) [] -- Scan.repeat (\<^keyword>\accepts\ |-- Parse.term) -- Scan.repeats ((\<^keyword>\invariant\) |-- parse_invariants)) - ) - >> (fn (((overloaded, hdr), (parent, attrs)),((rejects,accept_rex),invars)) => - Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} hdr parent - attrs rejects accept_rex invars))); + ) + + +val _ = + Outer_Syntax.command \<^command_keyword>\doc_class\ + "define document class" + (parse_doc_class >> (Toplevel.theory o add_doc_class_cmd')); + + +(*just an alternative syntax*) +val _ = + Outer_Syntax.command \<^command_keyword>\onto_class\ + "define ontological class" + (parse_doc_class >> (Toplevel.theory o add_doc_class_cmd')); + + end (* struct *) \ diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy index ca1f522..1bbdfe7 100755 --- a/src/DOF/RegExpInterface.thy +++ b/src/DOF/RegExpInterface.thy @@ -152,6 +152,7 @@ text\Here comes the hic : The reflection of the HOL-Automata module into a with an abstract interface hiding some generation artefacts like the internal states of the deterministic automata ...\ + ML\ structure RegExpInterface : sig