From 0f36e8b7612998f21213190c55add2ca0e5d5519 Mon Sep 17 00:00:00 2001 From: bu Date: Fri, 24 Aug 2018 17:14:39 +0200 Subject: [PATCH] Milestone reached: - further debugging - all tests checked - all examples running (after updates to current attribute conventions) --- Isa_DOF.thy | 12 +++++++----- examples/cenelec/Example.thy | 8 +++++--- examples/math_exam/BAC2017/BAC2017.thy | 12 ++++++------ examples/math_exam/MathExam/MathExam.thy | 6 +++--- examples/scholarly/IsaDofApplications.thy | 4 ++-- examples/simple/Concept_Example.thy | 2 +- 6 files changed, 24 insertions(+), 20 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 55fc663f..0c179a42 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -389,11 +389,13 @@ fun print_doc_items b ctxt = let val ({tab = x, ...},_)= get_data ctxt; val _ = writeln "====================================="; fun print_item (n, SOME({cid,id,pos,thy_name,value})) = - (writeln ("docitem: "^n); - writeln (" type: "^cid); - writeln (" origine: "^thy_name); - writeln (" value: " ^ (Syntax.string_of_term ctxt value)) - ); + (writeln ("docitem: "^n); + writeln (" type: "^cid); + writeln (" origine: "^thy_name); + writeln (" value: " ^ (Syntax.string_of_term ctxt value)) + ) + | print_item (n, NONE) = + (writeln ("forward reference for docitem: "^n)); in map print_item (Symtab.dest x); writeln "=====================================\n\n\n" end; diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index e76c1e85..4d96afee 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -19,8 +19,6 @@ text\ @{thm refl} of name @{thm [source] refl} section{* Example *} -print_doc_classes -print_doc_items text*[tralala] {* Brexit means Brexit *} @@ -52,7 +50,11 @@ declare_reference* [lalala::requirement, alpha="main", beta=42] declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] - + +print_doc_classes +print_doc_items + + paragraph* [sdfk] \ just a paragraph - lexical variant \ diff --git a/examples/math_exam/BAC2017/BAC2017.thy b/examples/math_exam/BAC2017/BAC2017.thy index a0c20e0f..a5276ef2 100644 --- a/examples/math_exam/BAC2017/BAC2017.thy +++ b/examples/math_exam/BAC2017/BAC2017.thy @@ -37,7 +37,7 @@ text{* text*[exo1 :: Exercise, - Exercise.concerns= "{setter,student,checker,externalExaminer}"] + concerns= "{setter,student,checker,externalExaminer}"] {* On considère la fonction h définie sur l’intervalle [0..+\] par : @{term "h(x) = x * exponent (-x)"} *} @@ -46,7 +46,7 @@ definition h :: "real \ real" where "h x \ x * exp (- x)" -text*[q1::Task, Task.concerns= "{setter,student}", +text*[q1::Task, concerns= "{setter,student}", level="oneStar", mark="1::int", type="formal"] {* Déterminer la limite de la fonction @{term h} en +\. *} @@ -57,7 +57,7 @@ lemma q1 : "(h \ (0::real)) at_top" sorry text*[v1::Validation, proofs="[@{thm ''q1''}::thm]"] {* See lemma @{thm q1}. *} -text*[q2::Task, Task.concerns= "{setter,checker,student}", +text*[q2::Task, concerns= "{setter,checker,student}", level="oneStar", mark="1::int", type="formal"] {* Étudier les variations de la fonction @{term h} sur l'intervalle [0..+\] et dresser son tableau de variation *} @@ -90,7 +90,7 @@ text*[v2::Validation, proofs="[@{thm ''q2_b''}, @{thm ''q2_c''}]"] {* See lemmas @{thm q2_b} and @{thm q2_c}. *} -text*[q3a::Task, Task.concerns= "{setter,checker,student}", +text*[q3a::Task, concerns= "{setter,checker,student}", level="oneStar", mark="1::int", type="formal"] {* Vérifier que pour tout nombre réel x appartenant à l'intervalle [0..+\], on a : @{term "h x = (exp (- x)) - (h' x)"}. *} @@ -106,8 +106,8 @@ subsubsection*[v3a::Validation, proofs="[@{thm ''q3a''}::thm]"] subsection*[sol1 :: Solution, - Solution.content="[exo1::Exercise]", - Solution.valids = "[v1::Validation,v2,v3a]"] + content="[exo1::Exercise]", + valids = "[v1::Validation,v2,v3a]"] {* See validations. *} diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index dede4e11..a060d745 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -36,7 +36,7 @@ figure*[figure::figure, spawn_columns=False,relative_width="''80''", \A Polynome.\ -subsubsection*[exo1 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 1\ +subsubsection*[exo1 :: Exercise, content="[q1::Task,q2::Task]"]\Exercise 1\ text{* Here are the first four lines of a number pattern. \begin{itemize} @@ -48,7 +48,7 @@ Here are the first four lines of a number pattern. *} declare [[show_sorts=false]] -subsubsection*[exo2 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 2\ +subsubsection*[exo2 :: Exercise, content="[q1::Task,q2::Task]"]\Exercise 2\ text{* Find the roots of the polynome: @{term "(x^3) - 6 * x^2 + 5 * x + 12"}. @@ -95,7 +95,7 @@ text*[a4::Answer_Formal_Step]{* Next Step: Fill in term and justification *} text*[q1::Task, level="oneStar", mark="1::int", type="formal"] {* Complete Line 10 : @{term "10*x + 2*y = 11*16"} *} -subsubsection*[exo3 :: Exercise, Exercise.content="[q1::Task,q2::Task]"]\Exercise 3\ +subsubsection*[exo3 :: Exercise, content="[q1::Task,q2::Task]"]\Exercise 3\ text*[q2::Task, level="threeStars", mark="3::int", type="formal"] {* Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index 033b9c0a..4446a736 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -93,7 +93,7 @@ we discuss the user-interaction generated from the ontological definitions. Fin conclusions and discuss related work in @{docitem_ref (unchecked) \conclusion\}. \ section*[bgrnd::text_section, - text_section.main_author="Some(@{docitem ''adb''}::author)"] + main_author="Some(@{docitem ''adb''}::author)"] \ Background: The Isabelle System \ text\ While Isabelle is widely perceived as an interactive theorem prover @@ -166,7 +166,7 @@ Isabelle's PIDE offers auto-completion and error-messages while typing the above \emph{semi-formal} content. \ section*[isadof::text_section, - text_section.main_author="Some(@{docitem ''adb''}::author)"] + main_author="Some(@{docitem ''adb''}::author)"] \ \isadof \ text\ An \isadof document consists of three components: diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index cc317969..c0357dff 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -4,7 +4,7 @@ begin open_monitor*[struct::M] -section*[a::A, x = "''alpha''"] \ Lorem ipsum dolor sit amet, ... \ +section*[a::A, x = "3"] \ Lorem ipsum dolor sit amet, ... \ text*[c1::C, x = "''beta''"] \ ... suspendisse non arcu malesuada mollis, nibh morbi, ... \