forked from Isabelle_DOF/Isabelle_DOF
Intermediate status : some spacing works.
This commit is contained in:
parent
ac835ea028
commit
eaca1959ce
15
Isa_DOF.thy
15
Isa_DOF.thy
|
@ -511,7 +511,7 @@ fun write_ontology_latex_sty_template thy =
|
||||||
(* or parameterising with "env" ? ? ?*)
|
(* or parameterising with "env" ? ? ?*)
|
||||||
else ""
|
else ""
|
||||||
val content = String.concat(map write_class (Symtab.dest y))
|
val content = String.concat(map write_class (Symtab.dest y))
|
||||||
val _ = writeln content
|
(* val _ = writeln content -- for interactive testing only, breaks LaTeX compilation *)
|
||||||
in writeFile ("Isa-DOF."^curr_thy_name^".template.sty") content
|
in writeFile ("Isa-DOF."^curr_thy_name^".template.sty") content
|
||||||
end;
|
end;
|
||||||
|
|
||||||
|
@ -690,7 +690,9 @@ val improper = Scan.many is_improper;
|
||||||
|
|
||||||
val attribute =
|
val attribute =
|
||||||
Parse.position Parse.const
|
Parse.position Parse.const
|
||||||
-- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.term) "True";
|
--| improper
|
||||||
|
-- Scan.optional (Parse.$$$ "=" --| improper |-- Parse.!!! Parse.term) "True"
|
||||||
|
: ((string * Position.T) * string) parser;
|
||||||
|
|
||||||
val attribute_upd : (((string * Position.T) * string) * string) parser =
|
val attribute_upd : (((string * Position.T) * string) * string) parser =
|
||||||
Parse.position Parse.const
|
Parse.position Parse.const
|
||||||
|
@ -703,17 +705,18 @@ val reference =
|
||||||
|
|
||||||
|
|
||||||
val attributes =
|
val attributes =
|
||||||
(Parse.$$$ "["
|
((Parse.$$$ "["
|
||||||
-- improper
|
-- improper
|
||||||
|-- (reference --
|
|-- (reference --
|
||||||
(Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," ( attribute)))) []))
|
(Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," (improper |-- attribute)))) []))
|
||||||
--| Parse.$$$ "]" : meta_args_t parser
|
--| Parse.$$$ "]"
|
||||||
|
--| improper) : meta_args_t parser
|
||||||
|
|
||||||
val attributes_upd =
|
val attributes_upd =
|
||||||
(Parse.$$$ "["
|
(Parse.$$$ "["
|
||||||
-- improper
|
-- improper
|
||||||
|-- (reference --
|
|-- (reference --
|
||||||
(Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," attribute_upd))) []))
|
(Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," (improper |-- attribute_upd)))) []))
|
||||||
--| Parse.$$$ "]"
|
--| Parse.$$$ "]"
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -5,19 +5,27 @@ begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
title*[
|
title*[
|
||||||
tit::
|
tit::title]\<open>Using the Isabelle Ontology Framework\<close>
|
||||||
title]\<open>Using the Isabelle Ontology Framework\<close>
|
|
||||||
subtitle*[stit::subtitle]
|
subtitle*[stit::subtitle]
|
||||||
\<open>Linking the Formal with the Informal\<close>
|
\<open>Linking the Formal with the Informal\<close>
|
||||||
|
|
||||||
text*[adb::author,
|
text*[adb::author,
|
||||||
email="''a.brucker@sheffield.ac.uk''",orcid="''0000-0002-6355-1200''",affiliation="''The University of Sheffield, Sheffield, UK''"]\<open>Achim D. Brucker\<close>
|
email="''a.brucker@sheffield.ac.uk''",
|
||||||
text*[idir::author,email="''idir.aitsadoune@centralesupelec.fr''",affiliation="''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
|
orcid="''0000-0002-6355-1200''",
|
||||||
text*[paolo::author,email="''paolo.crisafulli@irt-systemx.fr''",affiliation="''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
|
affiliation="''The University of Sheffield, Sheffield, UK''"]\<open>Achim D. Brucker\<close>
|
||||||
text*[bu::author,email="''wolff@lri.fr''",affiliation="''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
|
text*[idir::author,
|
||||||
|
email="''idir.aitsadoune@centralesupelec.fr''",
|
||||||
|
affiliation="''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
|
||||||
|
text*[paolo::author,
|
||||||
|
email="''paolo.crisafulli@irt-systemx.fr''",
|
||||||
|
affiliation="''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
|
||||||
|
text*[bu::author,
|
||||||
|
email = "''wolff@lri.fr''",
|
||||||
|
affiliation="''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
|
||||||
|
|
||||||
|
|
||||||
text*[abs::abstract,keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
|
text*[abs::abstract,
|
||||||
|
keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
|
||||||
While Isabelle is mostly known as part of Isabelle/HOL (an interactive
|
While Isabelle is mostly known as part of Isabelle/HOL (an interactive
|
||||||
theorem prover), it actually provides a framework for developing a wide
|
theorem prover), it actually provides a framework for developing a wide
|
||||||
spectrum of applications. A particular strength
|
spectrum of applications. A particular strength
|
||||||
|
|
|
@ -88,8 +88,10 @@ doc_class article =
|
||||||
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
||||||
conclusion ~~
|
conclusion ~~
|
||||||
bibliography)"
|
bibliography)"
|
||||||
(*
|
|
||||||
|
(* breaks currently LaTeX compilation:
|
||||||
gen_sty_template
|
gen_sty_template
|
||||||
*)
|
*)
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue