forked from Isabelle_DOF/Isabelle_DOF
Added missing space to warning messages.
This commit is contained in:
parent
60c6782874
commit
df12a32624
|
@ -1654,9 +1654,9 @@ 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)(* HACK bu 29/6.19 *)
|
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
|
||||||
|
|
||||||
val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} ->
|
val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} ->
|
||||||
|
|
Loading…
Reference in New Issue