Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

another attempt to solve the performance bug
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-07-01 12:40:11 +02:00
parent db83359f88
commit a52639655f
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isa_DOF.thy
View File

@ -1540,7 +1540,7 @@ ML\<open> (* Setting in thy_output.ML a parser for the syntactic handling of the
val _ = Thy_Output.set_meta_args_parser
(fn thy => let val _ = writeln "META_ARGS_PARSING"
in (Scan.optional ( ODL_Command_Parser.attributes
in (Scan.optional (Document_Source.improper |-- ODL_Command_Parser.attributes
>> ODL_LTX_Converter.meta_args_2_string thy) "")
end); \<close>
@ -1657,7 +1657,7 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name =
in () end
else if DOF_core.is_declared_oid_global name thy
then (if #strict_checking str
then warning("declared but undefined document reference:"^name)
then warning("declared but undefined document reference:"^name)(* HACK bu 29/6.19 *)
else ())
else error("undefined document reference:"^name)
end

2
patches/thy_output.ML
View File

@ -388,7 +388,7 @@ fun present_thy options thy (segments: segment list) =
pred keywords (Token.content_of tok)))
-- (Document_Source.annotation |--
(Parse.!!!!
( (Document_Source.improper |-- (!meta_args_parser_hook thy))
( ( (!meta_args_parser_hook thy))
-- ( (Document_Source.improper -- locale -- Document_Source.improper)
|-- Parse.document_source )
--| Document_Source.improper_end)