diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 552003a5..9fdd3975 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1231,15 +1231,13 @@ fun calculate_attr_access_check ctxt attr oid pos = (* template *) val markup = docref_markup false oid id pos_decl; val _ = Context_Position.report ctxt pos markup; val (* (long_cid, attr_b,ty) = *) - {def_occurrence, long_name, typ=ty,def_pos} = + {long_name, typ=ty,...} = case DOF_core.get_attribute_info_local cid attr ctxt of SOME f => f | NONE => error ("attribute undefined for ref"^ oid) val proj_term = Const(long_name,dummyT --> ty) - val term = calculate_attr_access ctxt proj_term term - in (ML_Syntax.atomic o ML_Syntax.print_term) term end + in calculate_attr_access ctxt proj_term term end | NONE => error "identifier not a docitem reference" - val _ = Theory.setup (ML_Antiquotation.inline @{binding docitem_attr} @@ -1248,12 +1246,36 @@ val _ = Theory.setup --| (Scan.lift @{keyword "::"}) -- Scan.lift (Parse.position Args.name) >> - (fn(attr:string,(oid:string,pos)) => calculate_attr_access_check ctxt attr oid pos) + (fn(attr:string,(oid:string,pos)) + => (ML_Syntax.atomic o ML_Syntax.print_term) + (calculate_attr_access_check ctxt attr oid pos)) : string context_parser ) (ctxt, toks)) - ) -end\ + ) + +fun calculate_trace ctxt oid pos = + let fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S) + val term = calculate_attr_access_check ctxt "trace" oid pos + val string_pair_list = map conv (HOLogic.dest_list term) + val conv_2_ML = ML_Syntax.print_list(ML_Syntax.print_pair + ML_Syntax.print_string + ML_Syntax.print_string) + in conv_2_ML string_pair_list end + +val _ = Theory.setup + (ML_Antiquotation.inline @{binding trace_attribute} + (fn (ctxt,toks) => + (Scan.lift (Parse.position Args.name) + >> (fn(oid:string,pos) => ML_Syntax.atomic (calculate_trace ctxt oid pos)) + : string context_parser + ) + (ctxt, toks)) + ) +end + + +\ @@ -1419,8 +1441,7 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []); *) ML\ fold_aterms Term.add_free_names; - fold_aterms Term.add_var_names; -\ + fold_aterms Term.add_var_names;\ diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index 1e503ada..49f4f424 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -117,13 +117,7 @@ figure*[fig_B::figure, close_monitor*[figs1] text\Resulting trace in figs1: \ -ML\ fun conv_doc_class_string_pair (Const(@{const_name "Pair"},_) - $ Const(s,_) - $ S) = (s, HOLogic.dest_string S); - -map conv_doc_class_string_pair (HOLogic.dest_list @{docitem_attr trace::figs1}) \ - - +ML\@{trace_attribute figs1}\ print_doc_items print_doc_classes diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index 1168d094..78d59a58 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -737,13 +737,9 @@ and therefore granted with public funds within the scope of the Program ``Invest (*<*) close_monitor*[this] -text\Resulting trace in this: \ -ML\ -fun conv_doc_class_string_pair (Const(@{const_name "Pair"},_) - $ Const(s,_) - $ S) = (s, HOLogic.dest_string S); +text\Resulting trace in doc\_item ''this'': \ +ML\@{trace_attribute this}\ -map conv_doc_class_string_pair (HOLogic.dest_list @{docitem_attr trace::this}) \ end (*>*)