# HG changeset patch
# User wenzelm
# Date 1461154148 -7200
# Node ID b07c9f5d38027d0b69106e841bec7a7b6c75da71
# Parent  8de0ebee3f1c71aa246c0388b70aa28da3c633ad# Parent  e0fa59bbc956fae3edeb9d24dcde07dd49edf7de
merged

diff -r 8de0ebee3f1c -r b07c9f5d3802 NEWS
--- a/NEWS	Fri Apr 15 10:19:35 2016 +0200
+++ b/NEWS	Wed Apr 20 14:09:08 2016 +0200
@@ -52,6 +52,10 @@
 
 * Highlighting of entity def/ref positions wrt. cursor.
 
+* Document markup works across multiple Isar commands, e.g. the results
+established at the end of a proof are properly identified in the theorem
+statement.
+
 
 *** Isar ***
 
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Pure/Isar/bundle.ML	Wed Apr 20 14:09:08 2016 +0200
@@ -86,8 +86,12 @@
 local
 
 fun gen_includes get args ctxt =
-  let val decls = maps (get ctxt) args
-  in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end;
+  let val decls = maps (get ctxt) args in
+    ctxt
+    |> Context_Position.set_visible false
+    |> Attrib.local_notes "" [((Binding.empty, []), decls)] |> #2
+    |> Context_Position.restore_visible ctxt
+  end;
 
 fun gen_context get prep_decl raw_incls raw_elems gthy =
   let
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 20 14:09:08 2016 +0200
@@ -119,24 +119,27 @@
   fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
 
 datatype locale = Loc of {
-  (** static part **)
+  (* static part *)
+
+  (*type and term parameters*)
   parameters: (string * sort) list * ((string * typ) * mixfix) list,
-    (* type and term parameters *)
+  (*assumptions (as a single predicate expression) and defines*)
   spec: term option * term list,
-    (* assumptions (as a single predicate expression) and defines *)
   intros: thm option * thm option,
   axioms: thm list,
+  (*diagnostic device: theorem part of hypothetical body as specified by the user*)
   hyp_spec: Element.context_i list,
-    (* diagnostic device: theorem part of hypothetical body as specified by the user *)
-  (** dynamic part **)
+
+  (* dynamic part *)
+
+  (*syntax declarations*)
   syntax_decls: (declaration * serial) list,
-    (* syntax declarations *)
+  (*theorem declarations*)
   notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
-    (* theorem declarations *)
-  dependencies: ((string * (morphism * morphism)) * serial) list
-    (* locale dependencies (sublocale relation) in reverse order *),
+  (*locale dependencies (sublocale relation) in reverse order*)
+  dependencies: ((string * (morphism * morphism)) * serial) list,
+  (*mixin part of dependencies*)
   mixins: mixins
-    (* mixin part of dependencies *)
 };
 
 fun mk_locale ((parameters, spec, intros, axioms, hyp_spec),
@@ -446,33 +449,34 @@
 (** Public activation functions **)
 
 fun activate_declarations dep = Context.proof_map (fn context =>
-  let
-    val thy = Context.theory_of context;
-  in
-    roundup thy activate_syntax_decls Morphism.identity dep (Idents.get context, context)
-    |-> Idents.put
-  end);
+  context
+  |> Context_Position.set_visible_generic false
+  |> pair (Idents.get context)
+  |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep
+  |-> Idents.put
+  |> Context_Position.restore_visible_generic context);
 
 fun activate_facts export dep context =
-  let
-    val thy = Context.theory_of context;
-    val activate =
-      activate_notes Element.init'
-        (Morphism.transfer_morphism o Context.theory_of) context export;
-  in
-    roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
-    |-> Idents.put
-  end;
+  context
+  |> Context_Position.set_visible_generic false
+  |> pair (Idents.get context)
+  |> roundup (Context.theory_of context)
+      (activate_notes Element.init' (Morphism.transfer_morphism o Context.theory_of) context export)
+      (the_default Morphism.identity export) dep
+  |-> Idents.put
+  |> Context_Position.restore_visible_generic context;
 
 fun init name thy =
   let
     val context = Context.Proof (Proof_Context.init_global thy);
     val marked = Idents.get context;
-    val (marked', context') = (empty_idents, context)
-      |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of);
   in
-    context'
-    |> Idents.put (merge_idents (marked, marked'))
+    context
+    |> Context_Position.set_visible_generic false
+    |> pair empty_idents
+    |> activate_all name thy Element.init' (Morphism.transfer_morphism o Context.theory_of)
+    |-> (fn marked' => Idents.put (merge_idents (marked, marked')))
+    |> Context_Position.restore_visible_generic context
     |> Context.proof_of
   end;
 
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 20 14:09:08 2016 +0200
@@ -564,11 +564,9 @@
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
     private def other_id(id: Document_ID.Generic)
-      : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = None
-    /* FIXME
+      : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] =
       (execs.get(id) orElse commands.get(id)).map(st =>
         ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk)))
-    */
 
     private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
       (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Pure/context_position.ML	Wed Apr 20 14:09:08 2016 +0200
@@ -14,6 +14,7 @@
   val set_visible_global: bool -> theory -> theory
   val is_really_visible: Proof.context -> bool
   val not_really: Proof.context -> Proof.context
+  val restore_visible_generic: Context.generic -> Context.generic -> Context.generic
   val restore_visible: Proof.context -> Proof.context -> Proof.context
   val restore_visible_global: theory -> theory -> theory
   val is_reported_generic: Context.generic -> Position.T -> bool
@@ -49,6 +50,7 @@
 fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt;
 val not_really = Context.proof_map (Data.map (apfst (K (SOME false))));
 
+val restore_visible_generic = Data.put o Data.get;
 val restore_visible = Context.proof_map o Data.put o Data.get o Context.Proof;
 val restore_visible_global = Context.theory_map o Data.put o Data.get o Context.Theory;
 
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Apr 20 14:09:08 2016 +0200
@@ -63,8 +63,8 @@
   def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
 
   val rich_text_area =
-    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
-      () => None, caret_visible = true, enable_hovering = false)
+    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
+      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
 
 
   /* perspective */
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Apr 20 14:09:08 2016 +0200
@@ -81,7 +81,7 @@
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
-      get_search_pattern _, caret_visible = false, enable_hovering = true)
+      get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
 
   private var current_search_pattern: Option[Regex] = None
   def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
diff -r 8de0ebee3f1c -r b07c9f5d3802 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Apr 15 10:19:35 2016 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Apr 20 14:09:08 2016 +0200
@@ -32,6 +32,7 @@
   get_rendering: () => Rendering,
   close_action: () => Unit,
   get_search_pattern: () => Option[Regex],
+  caret_update: () => Unit,
   caret_visible: Boolean,
   enable_hovering: Boolean)
 {
@@ -129,6 +130,7 @@
         new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
 
       if (new_text_info != old_text_info) {
+        caret_update()
         if (cursor.isDefined) {
           if (new_text_info.isDefined)
             text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get))