Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PIDE reports of implicit variable scope;
authorwenzelm
Tue, 05 Jul 2016 20:51:02 +0200
changeset 63396 ae07cd27ebf1
parent 63395 734723445a8c
child 63397 a528d24826c5
PIDE reports of implicit variable scope;
src/Pure/Isar/specification.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/specification.ML	Tue Jul 05 14:20:27 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Jul 05 20:51:02 2016 +0200
@@ -122,7 +122,12 @@
   in ((vars, xs), ctxt'') end;
 
 fun close_form ctxt ys prems concl =
-  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
+  let
+    val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
+
+    val pos_props = Logic.strip_imp_concl concl :: Logic.strip_imp_prems concl @ prems;
+    fun get_pos x = maps (get_positions ctxt x) pos_props;
+    val _ = Context_Position.reports ctxt (maps (Syntax_Phases.reports_of_scope o get_pos) xs);
   in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
 
 fun dummy_frees ctxt xs tss =
isabelle