adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

autolevity: avoid overlapping position info 

The @{here} antiquotation position leads to overlapping position
information which confuses the Isabelle session manager.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2021-01-28 15:39:02 +11:00 committed by Gerwin Klein
parent 4bf1635b2f
commit 77b4881697
2 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/AutoLevity_Base.thy
View File

@ -16,8 +16,8 @@ fun is_simp (_: Proof.context) (_: thm) = true
ML \<open>
val is_simp_installed = is_some (
try (ML_Context.eval ML_Compiler.flags @{here})
(ML_Lex.read_text ("val is_simp = Raw_Simplifier.is_simp", @{here} )));
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("val is_simp = Raw_Simplifier.is_simp", Position.none )));
\<close>
ML\<open>
@ -449,12 +449,12 @@ val post_apply_hook = (fn ctxt => fn text => fn pre_thm => fn post_thm =>
can work without them. Here we graciously fail if the hook interface is missing *)
fun setup_pre_apply_hook () =
try (ML_Context.eval ML_Compiler.flags @{here})
(ML_Lex.read_text ("Proof.set_pre_apply_hook AutoLevity_Base.pre_apply_hook", @{here}));
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("Proof.set_pre_apply_hook AutoLevity_Base.pre_apply_hook", Position.none));
fun setup_post_apply_hook () =
try (ML_Context.eval ML_Compiler.flags @{here})
(ML_Lex.read_text ("Proof.set_post_apply_hook AutoLevity_Base.post_apply_hook", @{here}));
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("Proof.set_post_apply_hook AutoLevity_Base.post_apply_hook", Position.none));
(* This command is treated specially by AutoLevity_Theory_Report. The command executed directly
after this one will be tagged with the given tag *)

7
lib/AutoLevity_Hooks.thy
View File

@ -136,7 +136,7 @@ in
end;
(* Wrapper that outputs to the Isabelle build log directory *)
fun levity_session_log () =
fun levity_session_log _ =
let
val this_session = Session.get_name ();
val fname = this_session ^ ".lev";
@ -156,6 +156,7 @@ handle exn =>
(Runtime.exn_message_list exn);
Exn.reraise exn);
end
\<close>
@ -163,8 +164,8 @@ end
The session shutdown hook requires a patch to Isabelle, so we wrap
this code to be a no-op on vanilla Isabelle installations. *)
ML \<open>
try (ML_Context.eval ML_Compiler.flags @{here})
(ML_Lex.read_text ("Session.register_shutdown_hook AutoLevity_Combined_Report.levity_session_log", @{here}))
try (ML_Context.eval ML_Compiler.flags Position.none)
(ML_Lex.read_text ("Session.register_shutdown_hook AutoLevity_Combined_Report.levity_session_log", Position.none))
\<close>
end