--- 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 ***
--- 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
--- 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;
--- 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) =>
--- 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;
--- 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 */
--- 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 }
--- 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))