diff --git a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy index 226d5a0..f2efeaf 100644 --- a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy +++ b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy @@ -3,7 +3,7 @@ theory IsaDofManual imports "../../../ontologies/technical_report" begin -open_monitor*[this::article] +open_monitor*[this::report] (*>*) title*[tit::title]\The \isadof User and Implementation Manual\ diff --git a/examples/technical_report/TR_my_commented_isabelle/output/document.pdf b/examples/technical_report/TR_my_commented_isabelle/output/document.pdf index 782eafa..0a935e7 100644 Binary files a/examples/technical_report/TR_my_commented_isabelle/output/document.pdf and b/examples/technical_report/TR_my_commented_isabelle/output/document.pdf differ diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index bb7a6f0..66a773b 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -25,17 +25,20 @@ doc_class abstract = doc_class text_section = main_author :: "author option" <= None fixme_list :: "string list" <= "[]" + level :: "int option" <= "None" + (* we follow LaTeX terminology on levels + part = Some -1 + chapter = Some 0 + section = Some 1 + subsection = Some 2 + subsubsection = Some 3 + ... *) + (* for scholarly paper: invariant level > 0 *) doc_class introduction = text_section + comment :: string claims :: "thm list" -doc_class introduction_title = introduction + - fixme_list :: "string list" <= "[]" - -doc_class introduction_elem = introduction + - fixme_list :: "string list" <= "[]" - doc_class technical = text_section + definition_list :: "string list" <= "[]" formal_results :: "thm list" @@ -84,16 +87,14 @@ text \underlying idea: a monitor class automatically receives a doc_class article = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" - accepts "(title ~~ - \subtitle\ ~~ - \author\\<^sup>+ ~~ - abstract ~~ - introduction_title ~~ - \introduction_elem\\<^sup>+ ~~ - \technical || example\\<^sup>+ ~~ - \introduction\ ~~ - conclusion ~~ - bibliography)" + accepts "(title ~~ + \subtitle\ ~~ + \author\\<^sup>+ ~~ + abstract ~~ + introduction ~~ + \technical || example\\<^sup>+ ~~ + conclusion ~~ + bibliography)" gen_sty_template diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index e64319a..b4fed9d 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -4,15 +4,19 @@ theory technical_report imports "scholarly_paper" begin +(* for reports paper: invariant: level \ -1 *) + doc_class table_of_contents = - depth :: int <= 3 + bookmark_depth :: int <= 3 + depth :: int <= 3 doc_class front_matter = - style :: string + front_matter_style :: string (* TODO Achim :::: *) + +doc_class index = + kind :: "doc_class" + level :: "int option" -doc_class "chapter" = text_section + - style :: string - doc_class report = style_id :: string <= "''LNCS''" version :: "(int \ int \ int)" <= "(0,0,0)" @@ -25,7 +29,7 @@ doc_class report = introduction ~~ \technical || example\\<^sup>+ ~~ conclusion ~~ - \table_of_contents\ ~~ + \index\\<^sup>+ ~~ bibliography)" end