Added open/close monitor syntax.
This commit is contained in:
parent
4d09fc5e34
commit
229997d60a
12
Isa_DOF.thy
12
Isa_DOF.thy
|
@ -11,7 +11,8 @@ that provide direct support in the PIDE framework. *}
|
|||
theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||
imports Main (* Isa_MOF *)
|
||||
keywords "section*" "subsection*" "subsubsection*"
|
||||
"paragraph*" "subparagraph*" "text*" "declare_reference"::thy_decl
|
||||
"paragraph*" "subparagraph*" "text*"
|
||||
"open_monitor" "close_monitor" "declare_reference"::thy_decl
|
||||
and
|
||||
"doc_class" :: thy_decl
|
||||
|
||||
|
@ -387,6 +388,15 @@ val _ =
|
|||
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "open_monitor"} "open a document reference monitor"
|
||||
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword "close_monitor"} "close a document reference monitor"
|
||||
(attributes >> (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (I)))); (* dummy so far *)
|
||||
|
||||
end (* struct *)
|
||||
|
||||
*}
|
||||
|
|
|
@ -1,6 +1,8 @@
|
|||
theory Article
|
||||
imports "../../ontologies/LNCS_onto"
|
||||
begin
|
||||
|
||||
open_monitor[onto::article]
|
||||
|
||||
text*[tit::title]{* Using The Isabelle Ontology Framework*}
|
||||
|
||||
|
@ -36,28 +38,12 @@ subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood.
|
|||
|
||||
subsection*[mathex_onto::example]{* Math-Exercise *}
|
||||
|
||||
subsection*[cenelec_onto::example]{* CENELEC *}
|
||||
|
||||
section*[con::conclusion]{* Future Work: Monitoring Classes *}
|
||||
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ...
|
||||
|
||||
The control of monitors is done by the commands:
|
||||
\<bullet> open_monitor <doc-class>
|
||||
\<bullet> close_monitor <doc-class>
|
||||
where the automaton of the monitor class is expected
|
||||
to be in a final state.
|
||||
|
||||
Monitors can be nested, so it is possible to "overlay" one or more monitoring
|
||||
classes and imposing different sets of structural constraints in a
|
||||
|
||||
Classes neither directly or via inheritance indirectly
|
||||
mentioned in the monitor are @{bold \<open>nested\<close>}
|
||||
from a monitor and may occur freely.
|
||||
*}
|
||||
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *}
|
||||
|
||||
subsection*[related::related_work]{* Related Work *}
|
||||
text{*
|
||||
\<bullet> XML and dtd's,
|
||||
\<bullet> @{bold \<open>XML\<close>} and dtd's,
|
||||
\<bullet> OWL and Protege,
|
||||
\<bullet> LaTeX setups such as ...
|
||||
@{url "https://pdi.fbk.eu/technologies/tex-owl-latex-style-syntax-authoring-owl-2-ontologies"}
|
||||
|
@ -66,8 +52,11 @@ text{*
|
|||
\<bullet> AADL Alisa,
|
||||
\<bullet> RATP Ovado
|
||||
*}
|
||||
|
||||
subsection{* Discussion *}
|
||||
|
||||
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *}
|
||||
|
||||
close_monitor[onto]
|
||||
|
||||
end
|
||||
|
||||
|
|
Loading…
Reference in New Issue