From 8ea00650a56a9d98cc102c5e1ffe4c8d43b2f405 Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 19 Apr 2018 11:04:11 +0200 Subject: [PATCH] Minor corrections, refactoring, steps towards attribute calculation. --- Isa_DOF.thy | 59 +++++++++++++++--------------------- MyCommentedIsabelle.thy | 5 +++ examples/cenelec/Example.thy | 2 +- examples/simple/MathExam.thy | 11 +++---- 4 files changed, 35 insertions(+), 42 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index e856250..80af240 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -92,7 +92,10 @@ struct father_is_sub s end - type docobj = {pos : Position.T, thy_name : string, id : serial, cid : string} + type docobj = {pos : Position.T, + thy_name : string, + value : term, + id : serial, cid : string} type docobj_tab ={tab : (docobj option) Symtab.table, maxano : int @@ -237,7 +240,7 @@ fun define_object_global (oid, bbb) thy = the space where it is ... *) in if is_defined_oid_global oid thy then error("multiple definition of document reference") - else map_data_global (apfst(fn {tab=t,maxano=x} => + else map_data_global (apfst(fn {tab=t,maxano=x} => {tab=Symtab.update(oid,SOME bbb) t, maxano=x})) (thy) @@ -303,14 +306,6 @@ end (* struct *) section{* Syntax for Annotated Documentation Commands (the '' View'' Part I) *} - -ML{* -fun read_terms ctxt = - grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt; - -map_filter; - -*} ML{* structure AnnoTextelemParser = @@ -356,34 +351,30 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs), val _ = Position.report pos (docref_markup true oid id pos); (* creates a markup label for this position and reports it to the PIDE framework; this label is used as jump-target for point-and-click feature. *) - fun handle_classref name (SOME(cid,pos')) thy = - let val _ = if not (DOF_core.is_defined_cid_global cid thy) - then error("document class undefined") - else () - val cid_long = DOF_core.name2doc_class_name thy cid - val {id, name=bind_target,...} = - the(DOF_core.get_doc_class_global cid_long thy) - val markup = docclass_markup false cid id (Binding.pos_of bind_target); - val ctxt = Context.Theory thy - val _ = Context_Position.report_generic ctxt pos' markup; - - - in DOF_core.define_object_global (oid, {pos=pos, thy_name=name, - id=id, cid=cid_long}) - (thy) - end - | handle_classref name NONE thy = - DOF_core.define_object_global - (oid, {pos=pos, thy_name=name, - id=id, cid=DOF_core.default_cid}) - (thy) + val undef = @{term "undefined"} + fun check_classref (SOME(cid,pos')) thy = + let val _ = if not (DOF_core.is_defined_cid_global cid thy) + then error("document class undefined") else () + val cid_long = DOF_core.name2doc_class_name thy cid + val {id, name=bind_target,...} = the(DOF_core.get_doc_class_global cid_long thy) + val markup = docclass_markup false cid id (Binding.pos_of bind_target); + val ctxt = Context.Theory thy + val _ = Context_Position.report_generic ctxt pos' markup; + in cid_long + end + | check_classref NONE _ = DOF_core.default_cid fun enrich_trans class_ref thy = let val name = Context.theory_name thy - fun read_assn ((lhs, pos), rhs) = (Syntax.read_term_global thy lhs, - Syntax.read_term_global thy rhs) + val cid_long = check_classref class_ref thy + fun read_assn ((lhs, pos), rhs) = ((Syntax.read_term_global thy lhs,pos), + Syntax.read_term_global thy rhs) val assns = map (read_assn ) doc_attrs - in thy |> handle_classref name class_ref + in thy |> DOF_core.define_object_global (oid, {pos=pos, + thy_name=name, + value = undef, + id=id, + cid=cid_long}) end fun MMM(SOME(s,p)) = SOME(s^"XXX",p) diff --git a/MyCommentedIsabelle.thy b/MyCommentedIsabelle.thy index ea906fe..badf2b5 100644 --- a/MyCommentedIsabelle.thy +++ b/MyCommentedIsabelle.thy @@ -289,6 +289,11 @@ Syntax.string_of_typ; Syntax.lookup_const; *} +ML{* +fun read_terms ctxt = + grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt; +*} + (* Main phases of inner syntax processing, with standard implementations of parse/unparse operations. diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index 81d40d1..d5ab6cf 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -67,7 +67,7 @@ section{* Some Tests for Ontology Framework and its CENELEC Instance *} declare_reference* [lalala::requirement, alpha="main", beta=42] -declare_reference* [lalala::quod] (* shouldn't work *) +declare_reference* [lalala::quod] (* shouldn't work: multiple declaration *) declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] diff --git a/examples/simple/MathExam.thy b/examples/simple/MathExam.thy index ed9c8b3..91d82fa 100644 --- a/examples/simple/MathExam.thy +++ b/examples/simple/MathExam.thy @@ -4,11 +4,10 @@ begin open_monitor*[exam::MathExam] -text*[idir::Author, affiliation="CentraleSupelec"]{*Idir AIT SADOUNE*} - -text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="Exam number 1"] -{* Please follow directions carefully ans show all your work.*} +text*[idir::Author, affiliation="''CentraleSupelec''"]{*Idir AIT SADOUNE*} +text*[header::Header,examGrade="A1", examSubject= "algebra", examTitle="''Exam number 1''"] +{* Please follow directions carefully and show all your work.*} section*[exo1 :: Exercise, content="[q1,q2,q3]"]{* Exercise 1.*} text*[q1::Question, level="twoStars", mark="5"] @@ -24,9 +23,7 @@ Write in interval notation : @{term ''-3 < x < 5''} *} text*[q3::Question, level="oneStar", mark="5"] -{* -True or false : @{term ''0/8 = 0''} -*} +{* True or false : @{term ''0/8 = 0''} *} close_monitor*[exam]