forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
6534c36375
|
@ -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
|
val _ = Thy_Output.set_meta_args_parser
|
||||||
(fn thy => let val _ = writeln "META_ARGS_PARSING"
|
(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) "")
|
>> ODL_LTX_Converter.meta_args_2_string thy) "")
|
||||||
end); \<close>
|
end); \<close>
|
||||||
|
|
||||||
|
@ -1657,7 +1657,7 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name =
|
||||||
in () end
|
in () end
|
||||||
else if DOF_core.is_declared_oid_global name thy
|
else if DOF_core.is_declared_oid_global name thy
|
||||||
then (if #strict_checking str
|
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 ())
|
||||||
else error("undefined document reference:"^name)
|
else error("undefined document reference:"^name)
|
||||||
end
|
end
|
||||||
|
|
|
@ -388,7 +388,7 @@ fun present_thy options thy (segments: segment list) =
|
||||||
pred keywords (Token.content_of tok)))
|
pred keywords (Token.content_of tok)))
|
||||||
-- (Document_Source.annotation |--
|
-- (Document_Source.annotation |--
|
||||||
(Parse.!!!!
|
(Parse.!!!!
|
||||||
( (Document_Source.improper |-- (!meta_args_parser_hook thy))
|
( ( (!meta_args_parser_hook thy))
|
||||||
-- ( (Document_Source.improper -- locale -- Document_Source.improper)
|
-- ( (Document_Source.improper -- locale -- Document_Source.improper)
|
||||||
|-- Parse.document_source )
|
|-- Parse.document_source )
|
||||||
--| Document_Source.improper_end)
|
--| Document_Source.improper_end)
|
||||||
|
|
Reference in New Issue