diff --git a/Isa_DOF.thy b/Isa_DOF.thy index d89a3d0..2008a19 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -28,12 +28,17 @@ section{*Inner Syntax Antiquotations: Syntax *} typedecl "typ" typedecl "term" typedecl "thm" +typedecl "file" +typedecl "http" +typedecl "thy" -- \ and others in the future : file, http, thy, ... \ consts mk_typ :: "string \ typ" ("@{typ _}") consts mk_term :: "string \ term" ("@{term _}") consts mk_thm :: "string \ thm" ("@{thm _}") +consts mk_file :: "string \ file" ("@{file _}") +consts mk_thy :: "string \ thy" ("@{thy _}") consts mk_docitem :: "string \ 'a" ("@{docitem _}") diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy index 3389ae7..6b71636 100644 --- a/examples/simple/Article.thy +++ b/examples/simple/Article.thy @@ -4,8 +4,6 @@ theory Article begin (* >> *) -ML{* val keywords = Thy_Header.get_keywords' @{context}; -*} open_monitor*[onto::article] diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index 02ae737..3187304 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -18,37 +18,34 @@ doc_class author = affiliation :: "string" doc_class abstract = - keywordlist :: "string list" <= "[]" - + keywordlist :: "string list" <= "[]" + principal_theorems :: "thm list" doc_class text_section = main_author :: "author option" <= None - -(* -doc_class text_section = - main_author :: "string option" <= None - *) doc_class introduction = text_section + comment :: string doc_class technical = text_section + definition_list :: "string list" <= "[]" - formula :: "thm list" + formal_results :: "thm list" text{* A very rough formatting style could be modeled as follows:*} -datatype mesure = points "int" | inch "int" | textwidth "int" (* given by the inverse of the integer *) +datatype mesure = points "int" + | inch "int" (* divised by 100 *) + | cm "int" (* divised by 100 *) + | textwidth "int" (* given in percent *) -datatype placement = left | center | right +datatype alignment = left | center | right doc_class figure = text_section + - width :: "mesure option" <= "Some(textwidth 1)" - height :: "mesure option" <= "Some(textwidth 1)" - scale :: "int option" (* in per cent *) - "file" :: string - plmt :: placement - caption :: string + width :: "mesure option" <= "Some(textwidth 100)" + height :: "mesure option" <= "Some(textwidth 100)" + scale :: "int option" (* given in per cent *) + "file" :: "file" + plmt :: alignment <= center (* something similar on tables ? Idea: rough abstraction of table attributes in LaTeX *)