diff --git a/Isabelle_DOF-Example-I/IsaDofApplications.thy b/Isabelle_DOF-Example-I/IsaDofApplications.thy index 098ebc7..914243b 100644 --- a/Isabelle_DOF-Example-I/IsaDofApplications.thy +++ b/Isabelle_DOF-Example-I/IsaDofApplications.thy @@ -635,20 +635,20 @@ text\ We present a selection of interaction scenarios @{example \sc and @{example \cenelec_onto\} with Isabelle/PIDE instrumented by \<^isadof>. \ (*<*) -declare_reference*["text-elements"::float] +declare_reference*["text_elements"::float] declare_reference*["hyperlinks"::float] (*>*) subsection*[scholar_pide::example]\ A Scholarly Paper \ -text\ In @{float (unchecked) "text-elements"}~(a) -and @{float (unchecked) "text-elements"}~(b)we show how +text\ In @{float (unchecked) "text_elements"}~(a) +and @{float (unchecked) "text_elements"}~(b)we show how hovering over links permits to explore its meta-information. Clicking on a document class identifier permits to hyperlink into the corresponding class definition (@{float (unchecked) "hyperlinks"}~(a)); hovering over an attribute-definition (which is qualified in order to disambiguate; @{float (unchecked) "hyperlinks"}~(b)). \ -text*["text-elements"::float, +text*["text_elements"::float, main_caption="\Exploring text elements.\"] \ @{fig_content (width=53, height=5, caption="Exploring a reference of a text element.") "figures/Dogfood-II-bgnd1.png" diff --git a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy index 3c2cb4d..e36acc4 100644 --- a/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy +++ b/Isabelle_DOF-Examples-Extra/CENELEC_50128/mini_odo/mini_odo.thy @@ -102,13 +102,13 @@ text\ functioning of the system and for its integration into the system as a whole. In particular, we need to make the following assumptions explicit: \<^vs>\-0.3cm\\ -text*["perfect-wheel"::assumption] +text*["perfect_wheel"::assumption] \\<^item> the wheel is perfectly circular with a given, constant radius. \<^vs>\-0.3cm\\ -text*["no-slip"::assumption] +text*["no_slip"::assumption] \\<^item> the slip between the trains wheel and the track negligible. \<^vs>\-0.3cm\\ -text*["constant-teeth-dist"::assumption] +text*["constant_teeth_dist"::assumption] \\<^item> the distance between all teeth of a wheel is the same and constant, and \<^vs>\-0.3cm\\ -text*["constant-sampling-rate"::assumption] +text*["constant_sampling_rate"::assumption] \\<^item> the sampling rate of positions is a given constant.\ text\ @@ -126,13 +126,13 @@ text\ subsection\Capturing ``System Architecture.''\ -figure*["three-phase"::figure,relative_width="70",file_src="''figures/three-phase-odo.pdf''"] +figure*["three_phase"::figure,relative_width="70",file_src="''figures/three-phase-odo.pdf''"] \An odometer with three sensors \C1\, \C2\, and \C3\.\ text\ The requirements analysis also contains a document \<^doc_class>\SYSAD\ (\<^typ>\system_architecture_description\) that contains technical drawing of the odometer, - a timing diagram (see \<^figure>\three-phase\), and tables describing the encoding of the position + a timing diagram (see \<^figure>\three_phase\), and tables describing the encoding of the position for the possible signal transitions of the sensors \C1\, \C2\, and \C3\. \ @@ -146,7 +146,7 @@ text\ sub-system configuration. \ (*<*) -declare_reference*["df-numerics-encshaft"::figure] +declare_reference*["df_numerics_encshaft"::figure] (*>*) subsection\Capturing ``Required Performances.''\ text\ @@ -160,9 +160,9 @@ text\ The requirement analysis document describes the physical environment, the architecture of the measuring device, and the required format and precision of the measurements of the odometry - function as represented (see @{figure (unchecked) "df-numerics-encshaft"}).\ + function as represented (see @{figure (unchecked) "df_numerics_encshaft"}).\ -figure*["df-numerics-encshaft"::figure,relative_width="76",file_src="''figures/df-numerics-encshaft.png''"] +figure*["df_numerics_encshaft"::figure,relative_width="76",file_src="''figures/df-numerics-encshaft.png''"] \Real distance vs. discrete distance vs. shaft-encoder sequence\ @@ -215,7 +215,7 @@ text\ concepts such as Cauchy Sequences, limits, differentiability, and a very substantial part of classical Calculus. \SOME\ is the Hilbert choice operator from HOL; the definitions of the model parameters admit all possible positive values as uninterpreted constants. Our - \<^assumption>\perfect-wheel\ is translated into a calculation of the circumference of the + \<^assumption>\perfect_wheel\ is translated into a calculation of the circumference of the wheel, while \\s\<^sub>r\<^sub>e\<^sub>s\, the resolution of the odometer, can be calculated from the these parameters. HOL-Analysis permits to formalize the fundamental physical observables: \ diff --git a/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index a80b722..e9dd5fb 100644 --- a/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/Isabelle_DOF-Examples-Extra/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -807,7 +807,7 @@ text\ They reflect the Pure logic depicted in a number of presentations s Notated as logical inference rules, these operations were presented as follows: \ -text*["text-elements"::float, +text*["text_elements"::float, main_caption="\Kernel Inference Rules.\"] \ @{fig_content (width=48, caption="Pure Kernel Inference Rules I.") "figures/pure-inferences-I.pdf" diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy index 4a31928..7210ca5 100644 --- a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -390,11 +390,11 @@ text-latex\ ML\ fun gen_enriched_document_command3 name {body} cid_transform attr_transform markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + ((((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, xstring_opt:(xstring * Position.T) option), toks:Input.source list) = gen_enriched_document_command2 name {body=body} cid_transform attr_transform markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + ((((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, xstring_opt:(xstring * Position.T) option), toks) \ \Hack : drop second and thrd args.\ diff --git a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy index 511466a..c4dc9a5 100644 --- a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy +++ b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy @@ -382,11 +382,11 @@ text-latex\ ML\ fun gen_enriched_document_command3 name {body} cid_transform attr_transform markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + ((((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, xstring_opt:(xstring * Position.T) option), toks:Input.source list) = gen_enriched_document_command2 name {body=body} cid_transform attr_transform markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + ((((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, xstring_opt:(xstring * Position.T) option), toks) \ \Hack : drop second and thrd args.\ diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy index 16c1c90..276c08e 100644 --- a/Isabelle_DOF-Unit-Tests/TestKit.thy +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -38,7 +38,8 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark toks_list:Input.source list) : theory -> theory = let val toplvl = Toplevel.theory_toplevel - val (((oid,pos),cid_pos), doc_attrs) = meta_args + val ((binding,cid_pos), doc_attrs) = meta_args + val oid = Binding.name_of binding val oid' = if meta_args = ODL_Meta_Args_Parser.empty_meta_args then "output" else oid @@ -74,7 +75,7 @@ fun gen_enriched_document_command2 name {body} cid_transform attr_transform mark else Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = false} {define = true} - oid pos (cid_transform cid_pos) (attr_transform doc_attrs)) + binding (cid_transform cid_pos) (attr_transform doc_attrs)) (* ... generating the level-attribute syntax *) in handle_margs_opt #> (fn thy => (app (check_n_tex_text thy) toks_list; thy)) end; @@ -139,10 +140,10 @@ val _ = >> (Toplevel.theory o update_instance_command)); val _ = - let fun create_and_check_docitem ((((oid, pos),cid_pos),doc_attrs),src) thy = + let fun create_and_check_docitem (((binding,cid_pos),doc_attrs),src) thy = (Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline=true} - {define = false} oid pos (cid_pos) (doc_attrs) thy) + {define = false} binding (cid_pos) (doc_attrs) thy) handle ERROR msg => (if error_match src msg then (writeln ("Correct error: "^msg^": reported.");thy) else error"Wrong error reported") diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 3e224b5..a5e007f 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -429,11 +429,11 @@ fun convert_src_from_margs ctxt (X, (((str,_),value)::R)) = fun float_command (name, pos) descr cid = let fun set_default_class NONE = SOME(cid,pos) |set_default_class (SOME X) = SOME X - fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = + fun create_instance (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = true} - {define = true} oid pos (set_default_class cid_pos) doc_attrs + {define = true} binding (set_default_class cid_pos) doc_attrs fun generate_fig_ltx_ctxt ctxt cap_src oid body = Latex.macro0 "centering" @ body @@ -441,25 +441,31 @@ fun float_command (name, pos) descr cid = @ Latex.macro "label" (DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt) |> DOF_core.output_name |> Latex.string) - fun parse_and_tex (margs as (((oid, _),_), _), cap_src) ctxt = - (convert_src_from_margs ctxt margs) - |> pair (upd_caption (K Input.empty) #> convert_meta_args ctxt margs) - |> fig_content ctxt - |> generate_fig_ltx_ctxt ctxt cap_src oid - |> (Latex.environment ("figure") ) + fun parse_and_tex (margs as ((binding,_), _), cap_src) ctxt = + let val oid = Binding.name_of binding + in + (convert_src_from_margs ctxt margs) + |> pair (upd_caption (K Input.empty) #> convert_meta_args ctxt margs) + |> fig_content ctxt + |> generate_fig_ltx_ctxt ctxt cap_src oid + |> (Latex.environment ("figure") ) + end in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex end fun listing_command (name, pos) descr cid = let fun set_default_class NONE = SOME(cid,pos) |set_default_class (SOME X) = SOME X - fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = + fun create_instance (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = true} - {define = true} oid pos (set_default_class cid_pos) doc_attrs - fun parse_and_tex (margs as (((_, pos),_), _), _) _ = - ISA_core.err ("Not yet implemented.\n Please use text*[oid::listing]\\ instead.") pos + {define = true} binding (set_default_class cid_pos) doc_attrs + fun parse_and_tex (margs as ((binding,_), _), _) _ = + let val pos = Binding.pos_of binding + in + ISA_core.err ("Not yet implemented.\n Please use text*[oid::listing]\\ instead.") pos + end in Monitor_Command_Parser.onto_macro_cmd_command (name, pos) descr create_instance parse_and_tex end @@ -858,11 +864,11 @@ fun convert_meta_args ctxt (X, (((str,_),value) :: R)) = fun frame_command (name, pos) descr cid = let fun set_default_class NONE = SOME(cid,pos) |set_default_class (SOME X) = SOME X - fun create_instance ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = + fun create_instance (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = true} - {define = true} oid pos (set_default_class cid_pos) doc_attrs + {define = true} binding (set_default_class cid_pos) doc_attrs fun titles_src ctxt frametitle framesubtitle src = Latex.string "{" @ Document_Output.output_document ctxt {markdown = false} frametitle diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index efa7d84..ba42a64 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -747,11 +747,10 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms i , rejectS, reg_exps, invs')) end -fun define_object_global {define = define} ((oid, pos), instance) thy = +fun define_object_global {define = define} (binding, instance) thy = let - val binding = if Long_Name.is_qualified oid - then Binding.make (Long_Name.base_name oid, pos) - else Binding.make (oid, pos) + val oid = Binding.name_of binding + val pos = Binding.pos_of binding val _ = if oid = undefined_instance then error (oid ^ ": This name is reserved by the implementation" ^ Position.here pos) else () @@ -1411,11 +1410,10 @@ ML\ structure ODL_Meta_Args_Parser = struct -type meta_args_t = ((string * Position.T) * - (string * Position.T) option) - * ((string * Position.T) * string) list +type meta_args_t = (binding * (string * Position.T) option) + * ((string * Position.T) * string) list -val empty_meta_args = ((("", Position.none), NONE), []) +val empty_meta_args = ((Binding.empty, NONE), []) val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore); val improper = Scan.many is_improper; (* parses white-space and comments *) @@ -1435,7 +1433,7 @@ val attribute_upd : (((string * Position.T) * string) * string) parser = : (((string * Position.T) * string) * string) parser; val reference = - Parse.position Parse.name + Parse.binding --| improper -- Scan.option (Parse.$$$ "::" -- improper @@ -1553,7 +1551,7 @@ fun cid_2_cidType cid_long thy = in fold (fn x => fn y => Type(ty_name x,[y])) (fathers cid_long) \<^Type>\unit\ end -fun create_default_object thy oid class_name typ = +fun create_default_object thy binding class_name typ = let val purified_class_name = String.translate (fn #"." => "_" | x => String.implode [x]) class_name fun attr_to_s (binding, _, _) = purified_class_name ^ "_" @@ -1583,11 +1581,8 @@ fun create_default_object thy oid class_name typ = val term = test_class |> cons (Long_Name.qualify class_name makeN) |> space_implode Symbol.space val ctxt = Proof_Context.init_global thy val term' = term |> Syntax.parse_term ctxt |> DOF_core.elaborate_term' ctxt - (* rename oid to be compatible with binding naming policy *) - val clean_oid = translate_string (fn ":" => "_" | "-" => "_" | c => c); - val oid' = clean_oid oid - val parsed_prop = Const (\<^const_name>\Pure.eq\, dummyT) $ Free (oid', dummyT) $ term' - val raw_vars = [(Binding.name oid', SOME typ, NoSyn)] + val parsed_prop = Const (\<^const_name>\Pure.eq\, dummyT) $ Free (Binding.name_of binding, dummyT) $ term' + val raw_vars = [(binding, SOME typ, NoSyn)] val (_, vars_ctxt) = DOF_core.prep_decls Proof_Context.cert_var raw_vars ctxt val concl = Syntax.check_prop vars_ctxt parsed_prop in Logic.dest_equals concl |> snd end @@ -1685,8 +1680,9 @@ fun msg_intro get n oid cid = ("accepts clause " ^ Int.toString n ^ get (" not enabled for", " rejected") ^ " doc_class: " ^ cid) -fun register_oid_cid_in_open_monitors oid _ (name, pos') thy = +fun register_oid_cid_in_open_monitors binding (name, pos') thy = let + val oid = Binding.name_of binding val cid_long= name fun is_enabled (n, monitor_info) = if exists (DOF_core.is_subclass_global thy cid_long) @@ -1784,8 +1780,9 @@ fun register_oid_cid_in_open_monitors oid _ (name, pos') thy = DOF_core.Monitor_Info.map (fold update_info delta_autoS) end -fun check_invariants thy (oid, _) = +fun check_invariants thy binding = let + val oid = Binding.name_of binding val docitem_value = DOF_core.value_of oid thy val name = DOF_core.cid_of oid thy |> DOF_core.get_onto_class_cid thy |> (fst o fst) @@ -1866,8 +1863,9 @@ fun check_invariants thy (oid, _) = in thy end -fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oid pos cid_pos doc_attrs thy = +fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} binding cid_pos doc_attrs thy = let + val oid = Binding.name_of binding val (((name, args_cid), typ), pos') = check_classref is_monitor cid_pos thy val cid_pos' = (name, pos') val cid_long = fst cid_pos' @@ -1888,7 +1886,7 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi else let fun conv_attrs ((lhs, pos), rhs) = (YXML.content_of lhs,pos,"=", Syntax.parse_term (Proof_Context.init_global thy) rhs) val assns' = map conv_attrs doc_attrs - val defaults_init = create_default_object thy oid cid_long typ + val defaults_init = create_default_object thy binding cid_long typ fun conv (na, _(*ty*), parsed_term) =(Binding.name_of na, Binding.pos_of na, "=", parsed_term); val S = map conv (DOF_core.get_attribute_defaults cid_long thy); val (defaults, _(*ty*), _) = calc_update_term {mk_elaboration=false} @@ -1902,12 +1900,12 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi in (input_term, value_term') end else (\<^term>\()\, value_term') end in thy |> DOF_core.define_object_global - {define = define} ((oid, pos), DOF_core.make_instance + {define = define} (binding, DOF_core.make_instance (false, fst value_terms, (snd value_terms) |> value (Proof_Context.init_global thy), is_inline, args_cid, vcid)) - |> register_oid_cid_in_open_monitors oid pos (name, pos') + |> register_oid_cid_in_open_monitors binding (name, pos') |> (fn thy => if (* declare_reference* without arguments is not checked against invariants *) thy |> DOF_core.defined_of oid |> not @@ -1925,18 +1923,18 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi ex: text*[sdf]\ Lorem ipsum @{thm refl}\ *) |> (fn thy => if default_cid then thy else if Config.get_global thy DOF_core.invariants_checking - then check_invariants thy (oid, pos) else thy)) + then check_invariants thy binding else thy)) end end (* structure Docitem_Parser *) -fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = +fun meta_args_exec (meta_args as ((binding, cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = thy |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args then (K thy) else Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = true} {define = true} - oid pos (I cid_pos) (I doc_attrs)) + binding (I cid_pos) (I doc_attrs)) fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t pos thy = let @@ -2082,16 +2080,17 @@ end; (* structure Value_Command *) structure Monitor_Command_Parser = struct -fun update_instance_command (((oid, pos), cid_pos), +fun update_instance_command ((binding, cid_pos), doc_attrs: (((string*Position.T)*string)*string)list) thy : theory = - let val cid = let val DOF_core.Instance {cid,...} = + let val oid = Binding.name_of binding + val cid = let val DOF_core.Instance {cid,...} = DOF_core.get_instance_global oid thy val ctxt = Proof_Context.init_global thy val instances = DOF_core.get_instances ctxt val markup = DOF_core.get_instance_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) - val _ = Context_Position.report ctxt pos markup; + val _ = Context_Position.report ctxt (Binding.pos_of binding) markup; in cid end val default_cid = cid = DOF_core.default_cid val (((name, cid'), typ), pos') = Value_Command.Docitem_Parser.check_classref {is_monitor = false} @@ -2127,7 +2126,7 @@ fun update_instance_command (((oid, pos), cid_pos), ex: text*[sdf]\ Lorem ipsum @{thm refl}\ *) |> (fn thy => if default_cid then thy else if Config.get_global thy DOF_core.invariants_checking - then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) + then Value_Command.Docitem_Parser.check_invariants thy binding else thy) end @@ -2136,39 +2135,41 @@ fun update_instance_command (((oid, pos), cid_pos), them out into the COL -- bu *) -fun open_monitor_command ((((oid, pos), raw_parent_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = - let fun o_m_c oid pos params_cid_pos doc_attrs thy = +fun open_monitor_command (((binding, raw_parent_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = + let fun o_m_c binding params_cid_pos doc_attrs thy = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor=true} (* this is a monitor *) {is_inline=false} (* monitors are always inline *) {define=true} - oid pos params_cid_pos doc_attrs thy + binding params_cid_pos doc_attrs thy fun compute_enabled_set cid thy = let val DOF_core.Onto_Class X = DOF_core.get_onto_class_global' cid thy val ralph = RegExpInterface.alphabet (#rejectS X) val aalph = RegExpInterface.alphabet (#rex X) in (aalph, ralph, map (RegExpInterface.rexp_term2da thy aalph)(#rex X)) end - fun create_monitor_entry oid thy = + fun create_monitor_entry thy = let val cid = case raw_parent_pos of - NONE => ISA_core.err ("You must specified a monitor class.") pos + NONE => ISA_core.err ("You must specified a monitor class.") (Binding.pos_of binding) | SOME (raw_parent, _) => DOF_core.markup2string raw_parent |> DOF_core.get_onto_class_cid thy |> (fst o fst) val (accS, rejectS, aS) = compute_enabled_set cid thy - in DOF_core.add_monitor_info (Binding.make (oid, pos)) + in DOF_core.add_monitor_info binding (DOF_core.make_monitor_info (accS, rejectS, aS)) thy end in thy - |> o_m_c oid pos raw_parent_pos doc_attrs - |> create_monitor_entry oid + |> o_m_c binding raw_parent_pos doc_attrs + |> create_monitor_entry end; -fun close_monitor_command (args as (((oid, pos), cid_pos), +fun close_monitor_command (args as ((binding, cid_pos), _: (((string*Position.T)*string)*string)list)) thy = - let fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 + let val oid = Binding.name_of binding + val pos = Binding.pos_of binding + fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 in if i >= 1 then Value_Command.Docitem_Parser.msg thy @@ -2192,17 +2193,18 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), |> update_instance_command args |> tap (DOF_core.check_ml_invs cid_long oid {is_monitor=true}) |> (fn thy => if Config.get_global thy DOF_core.invariants_checking - then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) + then Value_Command.Docitem_Parser.check_invariants thy binding else thy) |> delete_monitor_entry end fun meta_args_2_latex thy sem_attrs transform_attr - ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = + (((binding, cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = (* for the moment naive, i.e. without textual normalization of attribute names and adapted term printing *) - let val l = DOF_core.get_instance_name_global lab thy |> DOF_core.output_name + let val lab = Binding.name_of binding + val l = DOF_core.get_instance_name_global lab thy |> DOF_core.output_name |> enclose "{" "}" |> prefix "label = " val ((cid_long, _), _) = case cid_opt of @@ -2272,7 +2274,7 @@ fun meta_args_2_latex thy sem_attrs transform_attr then (name, DOF_core.output_name value') else ISA_core.err ("Bad name of semantic attribute" ^ name ^ ": " ^ value - ^ ". Name must be ASCII") pos + ^ ". Name must be ASCII") (Binding.pos_of binding) else (name, value') end) in update_sem_std_attrs attrs attrs'' end val updated_sem_std_attrs = update_sem_std_attrs sem_attrs transformed_args @@ -2289,14 +2291,14 @@ fun meta_args_2_latex thy sem_attrs transform_attr (* level-attribute information management *) fun gen_enriched_document_cmd {inline} cid_transform attr_transform - ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory = + (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = inline} - {define = true} oid pos (cid_transform cid_pos) (attr_transform doc_attrs); + {define = true} binding (cid_transform cid_pos) (attr_transform doc_attrs); fun gen_enriched_document_cmd' {inline} cid_transform attr_transform - ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory = + (((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) : theory -> theory = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = inline} - {define = false} oid pos (cid_transform cid_pos) (attr_transform doc_attrs); + {define = false} binding (cid_transform cid_pos) (attr_transform doc_attrs); (* markup reports and document output *) @@ -2512,12 +2514,12 @@ ML\ structure ML_star_Command = struct -fun meta_args_exec (meta_args as (((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) ctxt = +fun meta_args_exec (meta_args as ((binding,cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) ctxt = ctxt |> (if meta_args = ODL_Meta_Args_Parser.empty_meta_args then (K ctxt) else Context.map_theory (Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor = false} {is_inline = true} - {define = true} oid pos (I cid_pos) (I doc_attrs))) + {define = true} binding (I cid_pos) (I doc_attrs))) val attributes_opt = Scan.option ODL_Meta_Args_Parser.attributes diff --git a/Isabelle_DOF/thys/manual/M_02_Background.thy b/Isabelle_DOF/thys/manual/M_02_Background.thy index 69cd237..68cdbf5 100644 --- a/Isabelle_DOF/thys/manual/M_02_Background.thy +++ b/Isabelle_DOF/thys/manual/M_02_Background.thy @@ -208,13 +208,13 @@ text\ in many features over-accomplishes the required features of \<^dof>. \ -figure*["fig:dof-ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\ +figure*["fig_dof_ide",relative_width="95",file_src="''figures/cicm2018-combined.png''"]\ The \<^isadof> IDE (left) and the corresponding PDF (right), showing the first page of~@{cite "brucker.ea:isabelle-ontologies:2018"}.\ text\ We call the present implementation of \<^dof> on the Isabelle platform \<^isadof> . - @{figure "fig:dof-ide"} shows a screen-shot of an introductory paper on + @{figure "fig_dof_ide"} shows a screen-shot of an introductory paper on \<^isadof>~@{cite "brucker.ea:isabelle-ontologies:2018"}: the \<^isadof> PIDE can be seen on the left, while the generated presentation in PDF is shown on the right. diff --git a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy index 1b0e167..859bd38 100644 --- a/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy +++ b/Isabelle_DOF/thys/manual/M_03_GuidedTour.thy @@ -477,7 +477,7 @@ on the level of generated \<^verbatim>\.aux\-files, which are not n error-message and compiling it with a consistent bibtex usually makes disappear this behavior. \ -subsection*["using-term-aq"::technical, main_author = "Some @{author ''bu''}"] +subsection*["using_term_aq"::technical, main_author = "Some @{author ''bu''}"] \Using Term-Antiquotations\ text\The present version of \<^isadof> is the first version that supports the novel feature of @@ -577,11 +577,11 @@ term antiquotations: \ (*<*) -declare_reference*["subsec:onto-term-ctxt"::technical] +declare_reference*["subsec_onto_term_ctxt"::technical] (*>*) text\They are text-contexts equivalents to the \<^theory_text>\term*\ and \<^theory_text>\value*\ commands - for term-contexts introduced in @{technical (unchecked) \subsec:onto-term-ctxt\}\ + for term-contexts introduced in @{technical (unchecked) \subsec_onto_term_ctxt\}\ subsection\A Technical Report with Tight Checking\ text\An example of tight checking is a small programming manual to document programming trick diff --git a/Isabelle_DOF/thys/manual/M_04_RefMan.thy b/Isabelle_DOF/thys/manual/M_04_RefMan.thy index 292b7fe..7c5d09c 100644 --- a/Isabelle_DOF/thys/manual/M_04_RefMan.thy +++ b/Isabelle_DOF/thys/manual/M_04_RefMan.thy @@ -164,7 +164,7 @@ text\ to and between ontological concepts. \ -subsection*["odl-manual0"::technical]\Some Isabelle/HOL Specification Constructs Revisited\ +subsection*["odl_manual0"::technical]\Some Isabelle/HOL Specification Constructs Revisited\ text\ As ODL is an extension of Isabelle/HOL, document class definitions can therefore be arbitrarily mixed with standard HOL specification constructs. To make this manual self-contained, we present @@ -231,7 +231,7 @@ corresponding type-name \<^boxed_theory_text>\0.foo\ is not. For th definition of a \<^boxed_theory_text>\doc_class\ reject problematic lexical overlaps.\ -subsection*["odl-manual1"::technical]\Defining Document Classes\ +subsection*["odl_manual1"::technical]\Defining Document Classes\ text\ A document class\<^bindex>\document class\ can be defined using the @{command "doc_class"} keyword: \<^item> \class_id\:\<^bindex>\class\_id@\class_id\\ a type-\name\ that has been introduced @@ -350,7 +350,7 @@ layout; these commands have to be wrapped into text\ \<^item> \obj_id\:\<^index>\obj\_id@\obj_id\\ (or \<^emph>\oid\\<^index>\oid!oid@\see obj_id\\ for short) a \<^emph>\name\ - as specified in @{technical \odl-manual0\}. + as specified in @{technical \odl_manual0\}. \<^item> \meta_args\ : \<^rail>\obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \ \<^item> \<^emph>\evaluator\: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML, @@ -465,10 +465,10 @@ text*[b::B'_test']\\ term*\@{B'_test' \b\}\ -declare_reference*["text-elements-expls"::technical] +declare_reference*["text_elements_expls"::technical] (*>*) -subsection*["subsec:onto-term-ctxt"::technical]\Ontological Term-Contexts and their Management\ +subsection*["subsec_onto_term_ctxt"::technical]\Ontological Term-Contexts and their Management\ text\ \<^item> \annotated_term_element\ \<^rail>\ @@ -503,9 +503,9 @@ for example). With the exception of the @{command "term*"}-command, the term-ant This expansion happens \<^emph>\before\ evaluation of the term, thus permitting executable HOL-functions to interact with meta-objects. The @{command "assert*"}-command allows for logical statements to be checked in the global context -(see @{technical (unchecked) \text-elements-expls\}). +(see @{technical (unchecked) \text_elements_expls\}). % TODO: -% Section reference @{docitem (unchecked) \text-elements-expls\} has not the right number +% Section reference @{docitem (unchecked) \text_elements_expls\} has not the right number This is particularly useful to explore formal definitions wrt. their border cases. For @{command "assert*"}, the evaluation of the term can be disabled with the \<^boxed_theory_text>\disable_assert_evaluation\ theory attribute: @@ -558,7 +558,7 @@ of this meta-object. The latter leads to a failure of the entire command. \ (*<*) -declare_reference*["sec:advanced"::technical] +declare_reference*["sec_advanced"::technical] (*>*) subsection\Status and Query Commands\ @@ -586,7 +586,7 @@ text\ The raw term will be available in the \input_term\ field of \<^theory_text>\print_doc_items\ output and, \<^item> \<^theory_text>\check_doc_global\ checks if all declared object references have been defined, all monitors are in a final state, and checks the final invariant - on all objects (cf. @{technical (unchecked) \sec:advanced\}) + on all objects (cf. @{technical (unchecked) \sec_advanced\}) \ subsection\Macros\ @@ -738,7 +738,7 @@ text\The command syntax follows the implicit convention to add a ``*'' to distinguish them from the (similar) standard Isabelle text-commands which are not ontology-aware.\ -subsection*["text-elements"::technical]\The Ontology \<^verbatim>\scholarly_paper\\ +subsection*["text_elements"::technical]\The Ontology \<^verbatim>\scholarly_paper\\ (*<*) ML\val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\ ML\writeln (DOF_core.print_doc_class_tree @@ -821,9 +821,9 @@ or \text*[\::example, main_author = "Some(@{author \bu\})"] \ \ \\} where \<^boxed_theory_text>\"''bu''"\ is a string presentation of the reference to the author -text element (see below in @{docitem (unchecked) \text-elements-expls\}). +text element (see below in @{docitem (unchecked) \text_elements_expls\}). % TODO: -% Section reference @{docitem (unchecked) \text-elements-expls\} has not the right number +% Section reference @{docitem (unchecked) \text_elements_expls\} has not the right number \ text\Some of these concepts were supported as command-abbreviations leading to the extension @@ -866,7 +866,7 @@ of Isabelle is its ability to handle both, and to establish links between both w Therefore, the formal assertion command has been integrated to capture some form of formal content.\ -subsubsection*["text-elements-expls"::example]\Examples\ +subsubsection*["text_elements_expls"::example]\Examples\ text\ While the default user interface for class definitions via the @@ -1018,9 +1018,9 @@ schemata: -section*["sec:advanced"::technical]\Advanced ODL Concepts\ +section*["sec_advanced"::technical]\Advanced ODL Concepts\ -subsection*["sec:example"::technical]\Example\ +subsection*["sec_example"::technical]\Example\ text\We assume in this section the following local ontology: @{boxed_theory_text [display]\ @@ -1089,11 +1089,11 @@ text\ \ (*<*) -declare_reference*["sec:monitors"::technical] -declare_reference*["sec:low_level_inv"::technical] +declare_reference*["sec_monitors"::technical] +declare_reference*["sec_low_level_inv"::technical] (*>*) -subsection*["sec:class_inv"::technical]\ODL Class Invariants\ +subsection*["sec_class_inv"::technical]\ODL Class Invariants\ text\ Ontological classes as described so far are too liberal in many situations. @@ -1144,7 +1144,7 @@ text\ Hence, the \<^boxed_theory_text>\inv1\ invariant is checked when the instance \<^boxed_theory_text>\testinv2\ is defined. - Now let's add some invariants to our example in \<^technical>\sec:example\. + Now let's add some invariants to our example in \<^technical>\sec_example\. For example, one would like to express that any instance of a \<^boxed_theory_text>\result\ class finally has a non-empty property list, if its \<^boxed_theory_text>\kind\ is \<^boxed_theory_text>\proof\, or that @@ -1178,22 +1178,22 @@ text\ declare[[invariants_checking_with_tactics = true]]\} There are still some limitations with this high-level syntax. For now, the high-level syntax does not support the checking of - specific monitor behaviors (see @{technical (unchecked) "sec:monitors"}). + specific monitor behaviors (see @{technical (unchecked) "sec_monitors"}). For example, one would like to delay a final error message till the closing of a monitor. For this use-case you can use low-level class invariants - (see @{technical (unchecked) "sec:low_level_inv"}). + (see @{technical (unchecked) "sec_low_level_inv"}). Also, for now, term-antiquotations can not be used in an invariant formula. \ -subsection*["sec:low_level_inv"::technical]\ODL Low-level Class Invariants\ +subsection*["sec_low_level_inv"::technical]\ODL Low-level Class Invariants\ text\ If one want to go over the limitations of the actual high-level syntax of the invariant, one can define a function using SML. A formulation, in SML, of the class-invariant \<^boxed_theory_text>\has_property\ - in \<^technical>\sec:class_inv\, defined in the supposedly \Low_Level_Syntax_Invariants\ theory + in \<^technical>\sec_class_inv\, defined in the supposedly \Low_Level_Syntax_Invariants\ theory (note the long name of the class), is straight-forward: @@ -1222,7 +1222,7 @@ val _ = Theory.setup (DOF_core.make_ml_invariant (check_result_inv, cid_long) \<^boxed_theory_text>\oid\ is bound to a variable here and can therefore not be statically expanded. \ -subsection*["sec:monitors"::technical]\ODL Monitors\ +subsection*["sec_monitors"::technical]\ODL Monitors\ text\ We call a document class with an \accepts_clause\ a \<^emph>\monitor\.\<^bindex>\monitor\ Syntactically, an \accepts_clause\\<^index>\accepts\_clause@\accepts_clause\\ contains a regular expression over class identifiers. @@ -1291,18 +1291,18 @@ text\ sections. For now, the high-level syntax of invariants does not support the checking of specific monitor behaviors like the one just described and you must use - the low-level class invariants (see @{technical "sec:low_level_inv"}). + the low-level class invariants (see @{technical "sec_low_level_inv"}). Low-level invariants checking can be set up to be triggered when opening a monitor, when closing a monitor, or both by using the \<^ML>\DOF_core.add_opening_ml_invariant\, \<^ML>\DOF_core.add_closing_ml_invariant\, or \<^ML>\DOF_core.add_ml_invariant\ commands respectively, to add the invariants to the theory context - (See @{technical "sec:low_level_inv"} for an example). + (See @{technical "sec_low_level_inv"} for an example). \ -subsection*["sec:queries_on_instances"::technical]\Queries On Instances\ +subsection*["sec_queries_on_instances"::technical]\Queries On Instances\ text\ Any class definition generates term antiquotations checking a class instance or @@ -1414,7 +1414,7 @@ text\ \ -section*["document-templates"::technical]\Defining Document Templates\ +section*["document_templates"::technical]\Defining Document Templates\ subsection\The Core Template\ text\ diff --git a/Isabelle_DOF/thys/manual/M_05_Implementation.thy b/Isabelle_DOF/thys/manual/M_05_Implementation.thy index fc1207a..b5dadd0 100644 --- a/Isabelle_DOF/thys/manual/M_05_Implementation.thy +++ b/Isabelle_DOF/thys/manual/M_05_Implementation.thy @@ -188,7 +188,7 @@ text\ section\Programming Class Invariants\ text\ - See \<^technical>\sec:low_level_inv\. + See \<^technical>\sec_low_level_inv\. \ section\Implementing Monitors\ @@ -203,7 +203,7 @@ text\ val next : automaton -> env -> cid -> automaton\} where \<^boxed_sml>\env\ is basically a map between internal automaton states and class-id's (\<^boxed_sml>\cid\'s). An automaton is said to be \<^emph>\enabled\ for a class-id, - iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During + iff it either occurs in its accept-set or its reject-set (see @{docitem "sec_monitors"}). During top-down document validation, whenever a text-element is encountered, it is checked if a monitor is \emph{enabled} for this class; in this case, the \<^boxed_sml>\next\-operation is executed. The transformed automaton recognizing the suffix is stored in \<^boxed_sml>\docobj_tab\ if @@ -228,7 +228,7 @@ text\ \expandafter\providekeycommand\csname isaDof.#1\endcsname}%\} The \<^LaTeX>-generator of \<^isadof> maps each \<^boxed_theory_text>\doc_item\ to an \<^LaTeX>-environment (recall - @{docitem "text-elements"}). As generic \<^boxed_theory_text>\doc_item\s are derived from the text element, + @{docitem "text_elements"}). As generic \<^boxed_theory_text>\doc_item\s are derived from the text element, the environment \inlineltx|isamarkuptext*| builds the core of \<^isadof>'s \<^LaTeX> implementation. \