--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 12 15:48:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 12 18:02:01 2013 +0200
@@ -496,42 +496,43 @@
val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
val _ =
- Query_Operation.register_parallel sledgehammerN
- (fn st => fn [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] =>
- (case try Toplevel.proof_of st of
- SOME state =>
- let
- val ctxt = Proof.context_of state
+ Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
+ (case try Toplevel.proof_of st of
+ SOME state =>
+ let
+ val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args;
+ val ctxt = Proof.context_of state
- val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
- val override_params =
- ([("timeout", [timeout_arg]),
- ("blocking", ["true"])] @
- (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
- then [("isar_proofs", [isar_proofs_arg])] else []) @
- (if debug then [("debug", ["false"])] else []) @
- (if verbose then [("verbose", ["false"])] else []) @
- (if overlord then [("overlord", ["false"])] else []))
- |> map (normalize_raw_param ctxt)
+ val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
+ val override_params =
+ ([("timeout", [timeout_arg]),
+ ("blocking", ["true"])] @
+ (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
+ then [("isar_proofs", [isar_proofs_arg])] else []) @
+ (if debug then [("debug", ["false"])] else []) @
+ (if verbose then [("verbose", ["false"])] else []) @
+ (if overlord then [("overlord", ["false"])] else []))
+ |> map (normalize_raw_param ctxt)
- val i = the_default 1 (Int.fromString subgoal_arg)
+ val i = the_default 1 (Int.fromString subgoal_arg)
- val {provers, ...} =
- get_params Normal ctxt
- (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
+ val {provers, ...} =
+ get_params Normal ctxt
+ (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)])
- fun run prover =
- let
- val prover_params = ("provers", [prover]) :: override_params
- val sledgehammer_params = get_params Normal ctxt prover_params
- val minimize = minimize_command prover_params i
- val (_, (_, state')) =
- state
- |> Proof.map_context (Config.put sledgehammer_result_request true)
- |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
- in Config.get (Proof.context_of state') sledgehammer_result end
+ fun run prover =
+ let
+ val prover_params = ("provers", [prover]) :: override_params
+ val sledgehammer_params = get_params Normal ctxt prover_params
+ val minimize = minimize_command prover_params i
+ val (_, (_, state')) =
+ state
+ |> Proof.map_context (Config.put sledgehammer_result_request true)
+ |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize
+ in output_result (Config.get (Proof.context_of state') sledgehammer_result) end
- in map (fn prover => fn () => run prover) provers end
- | NONE => error "Unknown proof context"));
+ val _ = Par_Exn.release_all (Par_List.map (Exn.interruptible_capture run) provers);
+ in () end
+ | NONE => error "Unknown proof context"));
end;
--- a/src/HOL/Unix/Unix.thy Mon Aug 12 15:48:57 2013 +0200
+++ b/src/HOL/Unix/Unix.thy Mon Aug 12 18:02:01 2013 +0200
@@ -843,8 +843,6 @@
neither owned nor writable by @{term user\<^isub>1}.
*}
-
-
definition
"invariant root path =
(\<exists>att dir.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/multi_map.scala Mon Aug 12 18:02:01 2013 +0200
@@ -0,0 +1,68 @@
+/* Title: Pure/General/multi_map.scala
+ Module: PIDE
+
+Maps with multiple entries per key.
+*/
+
+package isabelle
+
+import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
+
+
+object Multi_Map extends ImmutableMapFactory[Multi_Map]
+{
+ private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty)
+ override def empty[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
+
+ implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] =
+ new MapCanBuildFrom[A, B]
+}
+
+
+final class Multi_Map[A, +B] private(rep: Map[A, List[B]])
+ extends scala.collection.immutable.Map[A, B]
+ with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]]
+{
+ /* Multi_Map operations */
+
+ def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
+
+ def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
+ {
+ val bs = get_list(a)
+ if (bs.contains(b)) this
+ else new Multi_Map(rep + (a -> (b :: bs)))
+ }
+
+ def remove[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =
+ {
+ val bs = get_list(a)
+ if (bs.contains(b)) {
+ bs.filterNot(_ == b) match {
+ case Nil => new Multi_Map(rep - a)
+ case bs1 => new Multi_Map(rep + (a -> bs1))
+ }
+ }
+ else this
+ }
+
+
+ /* Map operations */
+
+ override def stringPrefix = "Multi_Map"
+
+ override def empty = Multi_Map.empty
+ override def isEmpty: Boolean = rep.isEmpty
+
+ override def keySet: Set[A] = rep.keySet
+
+ override def iterator: Iterator[(A, B)] =
+ for ((a, bs) <- rep.iterator; b <- bs.iterator) yield (a, b)
+
+ def get(a: A): Option[B] = get_list(a).headOption
+
+ def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
+
+ def - (a: A): Multi_Map[A, B] =
+ if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
+}
--- a/src/Pure/PIDE/document.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 12 18:02:01 2013 +0200
@@ -15,6 +15,32 @@
{
/** document structure **/
+ /* overlays -- print functions with arguments */
+
+ object Overlays
+ {
+ val empty = new Overlays(Map.empty)
+ }
+
+ final class Overlays private(rep: Map[Node.Name, Node.Overlays])
+ {
+ def apply(name: Document.Node.Name): Node.Overlays =
+ rep.getOrElse(name, Node.Overlays.empty)
+
+ private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays =
+ {
+ val node_overlays = f(apply(name))
+ new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays))
+ }
+
+ def insert(command: Command, fn: String, args: List[String]): Overlays =
+ update(command.node_name, _.insert(command, fn, args))
+
+ def remove(command: Command, fn: String, args: List[String]): Overlays =
+ update(command.node_name, _.remove(command, fn, args))
+ }
+
+
/* individual nodes */
type Edit[A, B] = (Node.Name, Node.Edit[A, B])
@@ -60,45 +86,22 @@
}
- /* overlays -- print functions with arguments */
-
- type Overlay = (Command, (String, List[String]))
+ /* node overlays */
object Overlays
{
- val empty = new Overlays(Map.empty)
+ val empty = new Overlays(Multi_Map.empty)
}
- final class Overlays private(rep: Map[Command, List[(String, List[String])]])
+ final class Overlays private(rep: Multi_Map[Command, (String, List[String])])
{
def commands: Set[Command] = rep.keySet
def is_empty: Boolean = rep.isEmpty
-
- def insert(cmd: Command, over: (String, List[String])): Overlays =
- {
- val overs = rep.getOrElse(cmd, Nil)
- if (overs.contains(over)) this
- else new Overlays(rep + (cmd -> (over :: overs)))
- }
-
- def remove(cmd: Command, over: (String, List[String])): Overlays =
- rep.get(cmd) match {
- case Some(overs) =>
- if (overs.contains(over)) {
- overs.filterNot(_ == over) match {
- case Nil => new Overlays(rep - cmd)
- case overs1 => new Overlays(rep + (cmd -> overs1))
- }
- }
- else this
- case None => this
- }
-
- def dest: List[Overlay] =
- (for {
- (cmd, overs) <- rep.iterator
- over <- overs
- } yield (cmd, over)).toList
+ def dest: List[(Command, (String, List[String]))] = rep.iterator.toList
+ def insert(cmd: Command, fn: String, args: List[String]): Overlays =
+ new Overlays(rep.insert(cmd, (fn, args)))
+ def remove(cmd: Command, fn: String, args: List[String]): Overlays =
+ new Overlays(rep.remove(cmd, (fn, args)))
}
@@ -205,12 +208,6 @@
def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
command_range(range.start) takeWhile { case (_, start) => start < range.stop }
- def command_at(i: Text.Offset): Option[(Command, Text.Offset)] =
- {
- val range = command_range(i)
- if (range.hasNext) Some(range.next) else None
- }
-
def command_start(cmd: Command): Option[Text.Offset] =
Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2)
}
@@ -324,17 +321,23 @@
/** global state -- document structure, execution process, editing history **/
+ object Snapshot
+ {
+ val init = State.init.snapshot()
+ }
+
abstract class Snapshot
{
val state: State
val version: Version
- val node_name: Node.Name
- val node: Node
val is_outdated: Boolean
def convert(i: Text.Offset): Text.Offset
def revert(i: Text.Offset): Text.Offset
def convert(range: Text.Range): Text.Range
def revert(range: Text.Range): Text.Range
+
+ val node_name: Node.Name
+ val node: Node
def eq_content(other: Snapshot): Boolean
def cumulate_markup[A](
range: Text.Range,
@@ -555,10 +558,10 @@
new Snapshot
{
+ /* global information */
+
val state = State.this
val version = stable.version.get_finished
- val node_name = name
- val node = version.nodes(name)
val is_outdated = !(pending_edits.isEmpty && latest == stable)
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
@@ -566,6 +569,12 @@
def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
+
+ /* local node content */
+
+ val node_name = name
+ val node = version.nodes(name)
+
def eq_content(other: Snapshot): Boolean =
!is_outdated && !other.is_outdated &&
node.commands.size == other.node.commands.size &&
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/editor.scala Mon Aug 12 18:02:01 2013 +0200
@@ -0,0 +1,29 @@
+/* Title: Pure/PIDE/editor.scala
+ Author: Makarius
+
+General editor operations.
+*/
+
+package isabelle
+
+
+abstract class Editor[Context]
+{
+ def session: Session
+ def flush(): Unit
+ def current_context: Context
+ def current_node(context: Context): Option[Document.Node.Name]
+ def current_node_snapshot(context: Context): Option[Document.Snapshot]
+ def node_snapshot(name: Document.Node.Name): Document.Snapshot
+ def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)]
+
+ def node_overlays(name: Document.Node.Name): Document.Node.Overlays
+ def insert_overlay(command: Command, fn: String, args: List[String]): Unit
+ def remove_overlay(command: Command, fn: String, args: List[String]): Unit
+
+ abstract class Hyperlink { def follow(context: Context): Unit }
+ def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink
+ def hyperlink_command(
+ snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink]
+}
+
--- a/src/Pure/PIDE/query_operation.ML Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Pure/PIDE/query_operation.ML Mon Aug 12 18:02:01 2013 +0200
@@ -7,14 +7,14 @@
signature QUERY_OPERATION =
sig
- val register_parallel: string -> (Toplevel.state -> string list -> (unit -> string) list) -> unit
- val register: string -> (Toplevel.state -> string list -> string) -> unit
+ val register: string ->
+ ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit
end;
structure Query_Operation: QUERY_OPERATION =
struct
-fun register_parallel name f =
+fun register name f =
Command.print_function name
(fn {args = instance :: args, ...} =>
SOME {delay = NONE, pri = 0, persistent = false, strict = false,
@@ -22,23 +22,19 @@
let
fun result s = Output.result [(Markup.instanceN, instance)] s;
fun status m = result (Markup.markup_only m);
+ fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
fun toplevel_error exn =
result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
val _ = status Markup.running;
- val outputs =
- Multithreading.interruptible (fn () => f state args) ()
- handle exn (*sic!*) => (toplevel_error exn; []);
- val _ = outputs |> Par_List.map (fn out =>
- (case Exn.capture (restore_attributes out) () (*sic!*) of
- Exn.Res s => result (Markup.markup (Markup.writelnN, []) s)
- | Exn.Exn exn => toplevel_error exn));
+ fun run () = f {state = state, args = args, output_result = output_result};
+ val _ =
+ (case Exn.capture (*sic!*) (restore_attributes run) () of
+ Exn.Res () => ()
+ | Exn.Exn exn => toplevel_error exn);
val _ = status Markup.finished;
in () end)}
| _ => NONE);
-fun register name f =
- register_parallel name (fn st => fn args => [fn () => f st args]);
-
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/query_operation.scala Mon Aug 12 18:02:01 2013 +0200
@@ -0,0 +1,203 @@
+/* Title: Pure/PIDE/query_operation.scala
+ Author: Makarius
+
+One-shot query operations via asynchronous print functions and temporary
+document overlays.
+*/
+
+package isabelle
+
+
+import scala.actors.Actor._
+
+
+object Query_Operation
+{
+ object Status extends Enumeration
+ {
+ val WAITING = Value("waiting")
+ val RUNNING = Value("running")
+ val FINISHED = Value("finished")
+ }
+}
+
+class Query_Operation[Editor_Context](
+ editor: Editor[Editor_Context],
+ editor_context: Editor_Context,
+ operation_name: String,
+ consume_status: Query_Operation.Status.Value => Unit,
+ consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
+{
+ private val instance = Document_ID.make().toString
+
+
+ /* implicit state -- owned by Swing thread */
+
+ private var current_location: Option[Command] = None
+ private var current_query: List[String] = Nil
+ private var current_update_pending = false
+ private var current_output: List[XML.Tree] = Nil
+ private var current_status = Query_Operation.Status.FINISHED
+ private var current_exec_id = Document_ID.none
+
+ private def reset_state()
+ {
+ current_location = None
+ current_query = Nil
+ current_update_pending = false
+ current_output = Nil
+ current_status = Query_Operation.Status.FINISHED
+ current_exec_id = Document_ID.none
+ }
+
+ private def remove_overlay()
+ {
+ current_location.foreach(command =>
+ editor.remove_overlay(command, operation_name, instance :: current_query))
+ }
+
+
+ /* content update */
+
+ private def content_update()
+ {
+ Swing_Thread.require()
+
+
+ /* snapshot */
+
+ val (snapshot, state, removed) =
+ current_location match {
+ case Some(cmd) =>
+ val snapshot = editor.node_snapshot(cmd.node_name)
+ val state = snapshot.state.command_state(snapshot.version, cmd)
+ val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
+ (snapshot, state, removed)
+ case None =>
+ (Document.Snapshot.init, Command.empty.init_state, true)
+ }
+
+ val results =
+ (for {
+ (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
+ if props.contains((Markup.INSTANCE, instance))
+ } yield elem).toList
+
+
+ /* output */
+
+ val new_output =
+ for {
+ XML.Elem(_, List(XML.Elem(markup, body))) <- results
+ if Markup.messages.contains(markup.name)
+ } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
+
+
+ /* status */
+
+ def get_status(name: String, status: Query_Operation.Status.Value)
+ : Option[Query_Operation.Status.Value] =
+ results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
+
+ val new_status =
+ if (removed) Query_Operation.Status.FINISHED
+ else
+ get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
+ get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
+ Query_Operation.Status.WAITING
+
+ if (new_status == Query_Operation.Status.RUNNING)
+ results.collectFirst(
+ {
+ case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
+ if elem.name == Markup.RUNNING => id
+ }).foreach(id => current_exec_id = id)
+
+
+ /* state update */
+
+ if (current_output != new_output || current_status != new_status) {
+ if (snapshot.is_outdated)
+ current_update_pending = true
+ else {
+ current_update_pending = false
+ if (current_output != new_output && !removed) {
+ current_output = new_output
+ consume_output(snapshot, state.results, new_output)
+ }
+ if (current_status != new_status) {
+ current_status = new_status
+ consume_status(new_status)
+ if (new_status == Query_Operation.Status.FINISHED) {
+ remove_overlay()
+ editor.flush()
+ }
+ }
+ }
+ }
+ }
+
+
+ /* query operations */
+
+ def cancel_query(): Unit =
+ Swing_Thread.require { editor.session.cancel_exec(current_exec_id) }
+
+ def apply_query(query: List[String])
+ {
+ Swing_Thread.require()
+
+ editor.current_node_snapshot(editor_context) match {
+ case Some(snapshot) =>
+ remove_overlay()
+ reset_state()
+ consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+ editor.current_command(editor_context, snapshot) match {
+ case Some((command, _)) =>
+ current_location = Some(command)
+ current_query = query
+ current_status = Query_Operation.Status.WAITING
+ editor.insert_overlay(command, operation_name, instance :: query)
+ case None =>
+ }
+ consume_status(current_status)
+ editor.flush()
+ case None =>
+ }
+ }
+
+ def locate_query()
+ {
+ Swing_Thread.require()
+
+ for {
+ command <- current_location
+ snapshot = editor.node_snapshot(command.node_name)
+ link <- editor.hyperlink_command(snapshot, command)
+ } link.follow(editor_context)
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case changed: Session.Commands_Changed =>
+ current_location match {
+ case Some(command)
+ if current_update_pending ||
+ (current_status != Query_Operation.Status.FINISHED &&
+ changed.commands.contains(command)) =>
+ Swing_Thread.later { content_update() }
+ case _ =>
+ }
+ case bad =>
+ java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def activate() { editor.session.commands_changed += main_actor }
+ def deactivate() { editor.session.commands_changed -= main_actor }
+}
--- a/src/Pure/Tools/find_theorems.ML Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Aug 12 18:02:01 2013 +0200
@@ -575,17 +575,17 @@
(** PIDE query operation **)
val _ =
- Query_Operation.register "find_theorems"
- (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] =>
- if can Toplevel.context_of st then
- let
- val state =
- if context_arg = "" then proof_state st
- else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
- val opt_limit = Int.fromString limit_arg;
- val rem_dups = allow_dups_arg = "false";
- val criteria = read_query Position.none query_arg;
- in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end
- else error "Unknown context");
+ Query_Operation.register "find_theorems" (fn {state = st, args, output_result} =>
+ if can Toplevel.context_of st then
+ let
+ val [limit_arg, allow_dups_arg, context_arg, query_arg] = args;
+ val state =
+ if context_arg = "" then proof_state st
+ else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg));
+ val opt_limit = Int.fromString limit_arg;
+ val rem_dups = allow_dups_arg = "false";
+ val criteria = read_query Position.none query_arg;
+ in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end
+ else error "Unknown context");
end;
--- a/src/Pure/build-jars Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Pure/build-jars Mon Aug 12 18:02:01 2013 +0200
@@ -18,6 +18,7 @@
General/graph.scala
General/graphics_file.scala
General/linear_set.scala
+ General/multi_map.scala
General/path.scala
General/position.scala
General/pretty.scala
@@ -35,9 +36,11 @@
PIDE/command.scala
PIDE/document.scala
PIDE/document_id.scala
+ PIDE/editor.scala
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
+ PIDE/query_operation.scala
PIDE/text.scala
PIDE/xml.scala
PIDE/yxml.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Aug 12 18:02:01 2013 +0200
@@ -17,13 +17,13 @@
"src/fold_handling.scala"
"src/graphview_dockable.scala"
"src/html_panel.scala"
- "src/hyperlink.scala"
"src/info_dockable.scala"
"src/isabelle.scala"
"src/isabelle_encoding.scala"
"src/isabelle_logic.scala"
"src/isabelle_options.scala"
"src/isabelle_sidekick.scala"
+ "src/jedit_editor.scala"
"src/jedit_lib.scala"
"src/jedit_main.scala"
"src/jedit_options.scala"
@@ -36,7 +36,6 @@
"src/pretty_tooltip.scala"
"src/process_indicator.scala"
"src/protocol_dockable.scala"
- "src/query_operation.scala"
"src/raw_output_dockable.scala"
"src/readme_dockable.scala"
"src/rendering.scala"
--- a/src/Tools/jEdit/src/document_model.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Aug 12 18:02:01 2013 +0200
@@ -46,11 +46,11 @@
}
}
- def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
+ def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
{
Swing_Thread.require()
apply(buffer).map(_.deactivate)
- val model = new Document_Model(session, buffer, name)
+ val model = new Document_Model(session, buffer, node_name)
buffer.setProperty(key, model)
model.activate()
buffer.propertiesChanged
@@ -59,7 +59,7 @@
}
-class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
+class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
{
/* header */
@@ -68,7 +68,7 @@
Swing_Thread.require()
JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
- PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
+ PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
@@ -77,17 +77,6 @@
}
- /* overlays */
-
- private var overlays = Document.Node.Overlays.empty
-
- def insert_overlay(command: Command, name: String, args: List[String]): Unit =
- Swing_Thread.require { overlays = overlays.insert(command, (name, args)) }
-
- def remove_overlay(command: Command, name: String, args: List[String]): Unit =
- Swing_Thread.require { overlays = overlays.remove(command, (name, args)) }
-
-
/* perspective */
// owned by Swing thread
@@ -99,7 +88,7 @@
if (_node_required != b) {
_node_required = b
PIDE.options_changed()
- PIDE.flush_buffers()
+ PIDE.editor.flush()
}
}
@@ -115,7 +104,7 @@
for {
doc_view <- PIDE.document_views(buffer)
range <- doc_view.perspective().ranges
- } yield range), overlays)
+ } yield range), PIDE.editor.node_overlays(node_name))
}
else empty_perspective
}
@@ -131,10 +120,10 @@
val text = JEdit_Lib.buffer_text(buffer)
val perspective = node_perspective()
- List(session.header_edit(name, header),
- name -> Document.Node.Clear(),
- name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
- name -> perspective)
+ List(session.header_edit(node_name, header),
+ node_name -> Document.Node.Clear(),
+ node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
+ node_name -> perspective)
}
def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit])
@@ -144,9 +133,9 @@
val header = node_header()
- List(session.header_edit(name, header),
- name -> Document.Node.Edits(text_edits),
- name -> perspective)
+ List(session.header_edit(node_name, header),
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
}
@@ -208,7 +197,7 @@
def snapshot(): Document.Snapshot =
{
Swing_Thread.require()
- session.snapshot(name, pending_edits.snapshot())
+ session.snapshot(node_name, pending_edits.snapshot())
}
--- a/src/Tools/jEdit/src/document_view.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Aug 12 18:02:01 2013 +0200
@@ -197,7 +197,7 @@
val snapshot = model.snapshot()
if (changed.assignment ||
- (changed.nodes.contains(model.name) &&
+ (changed.nodes.contains(model.node_name) &&
changed.commands.exists(snapshot.node.commands.contains)))
Swing_Thread.later { overview.delay_repaint.invoke() }
--- a/src/Tools/jEdit/src/documentation_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -66,7 +66,7 @@
"Documentation error", GUI.scrollable_text(Exn.message(exn)))
})
case Text_File(_, path) =>
- Hyperlink(Isabelle_System.platform_path(path)).follow(view)
+ PIDE.editor.goto(view, Isabelle_System.platform_path(path))
case _ =>
}
case _ =>
--- a/src/Tools/jEdit/src/find_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -46,7 +46,7 @@
}
private val find_theorems =
- Query_Operation(view, "find_theorems", consume_status _,
+ new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
--- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -22,7 +22,7 @@
{
/* implicit arguments -- owned by Swing thread */
- private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_snapshot = Document.Snapshot.init
private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
private var implicit_graph = no_graph
@@ -36,7 +36,7 @@
}
private def reset_implicit(): Unit =
- set_implicit(Document.State.init.snapshot(), no_graph)
+ set_implicit(Document.Snapshot.init, no_graph)
def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
{
--- a/src/Tools/jEdit/src/hyperlink.scala Mon Aug 12 15:48:57 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-/* Title: Tools/jEdit/src/hyperlink.scala
- Author: Fabian Immler, TU Munich
- Author: Makarius
-
-Hyperlinks within jEdit buffers for PIDE proof documents.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.{View, jEdit}
-import org.gjt.sp.jedit.textarea.JEditTextArea
-
-
-object Hyperlink
-{
- def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
- File_Link(jedit_file, line, column)
-}
-
-abstract class Hyperlink
-{
- def follow(view: View): Unit
-}
-
-private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink
-{
- override def follow(view: View)
- {
- Swing_Thread.require()
-
- JEdit_Lib.jedit_buffer(jedit_file) match {
- case Some(buffer) =>
- view.goToBuffer(buffer)
- val text_area = view.getTextArea
-
- try {
- val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
- text_area.moveCaretPosition(line_start)
- if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
- }
- catch {
- case _: ArrayIndexOutOfBoundsException =>
- case _: IllegalArgumentException =>
- }
-
- case None =>
- val args =
- if (line <= 0) Array(jedit_file)
- else if (column <= 0) Array(jedit_file, "+line:" + line.toInt)
- else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt)
- jEdit.openFiles(view, null, args)
- }
- }
-}
-
--- a/src/Tools/jEdit/src/info_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -25,7 +25,7 @@
{
/* implicit arguments -- owned by Swing thread */
- private var implicit_snapshot = Document.State.init.snapshot()
+ private var implicit_snapshot = Document.Snapshot.init
private var implicit_results = Command.Results.empty
private var implicit_info: XML.Body = Nil
@@ -39,7 +39,7 @@
}
private def reset_implicit(): Unit =
- set_implicit(Document.State.init.snapshot(), Command.Results.empty, Nil)
+ set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
{
--- a/src/Tools/jEdit/src/isabelle.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Aug 12 18:02:01 2013 +0200
@@ -70,7 +70,7 @@
if (continuous_checking != b) {
PIDE.options.bool(CONTINUOUS_CHECKING) = b
PIDE.options_changed()
- PIDE.flush_buffers()
+ PIDE.editor.flush()
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Aug 12 18:02:01 2013 +0200
@@ -0,0 +1,149 @@
+/* Title: Tools/jEdit/src/jedit_editor.scala
+ Author: Makarius
+
+PIDE editor operations for jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+class JEdit_Editor extends Editor[View]
+{
+ /* session */
+
+ override def session: Session = PIDE.session
+
+ override def flush()
+ {
+ Swing_Thread.require()
+
+ session.update(
+ (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
+ case (edits, buffer) =>
+ JEdit_Lib.buffer_lock(buffer) {
+ PIDE.document_model(buffer) match {
+ case Some(model) => model.flushed_edits() ::: edits
+ case None => edits
+ }
+ }
+ }
+ )
+ }
+
+
+ /* current situation */
+
+ override def current_context: View =
+ Swing_Thread.require { jEdit.getActiveView() }
+
+ override def current_node(view: View): Option[Document.Node.Name] =
+ Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
+
+ override def current_node_snapshot(view: View): Option[Document.Snapshot] =
+ Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
+
+ override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
+ {
+ Swing_Thread.require()
+
+ JEdit_Lib.jedit_buffer(name.node) match {
+ case Some(buffer) =>
+ PIDE.document_model(buffer) match {
+ case Some(model) => model.snapshot
+ case None => session.snapshot(name)
+ }
+ case None => session.snapshot(name)
+ }
+ }
+
+ override def current_command(view: View, snapshot: Document.Snapshot)
+ : Option[(Command, Text.Offset)] =
+ {
+ Swing_Thread.require()
+
+ if (snapshot.is_outdated) None
+ else {
+ val text_area = view.getTextArea
+ PIDE.document_view(text_area) match {
+ case Some(doc_view) =>
+ val node = snapshot.version.nodes(doc_view.model.node_name)
+ val caret_commands = node.command_range(text_area.getCaretPosition)
+ if (caret_commands.hasNext) Some(caret_commands.next) else None
+ case None => None
+ }
+ }
+ }
+
+
+ /* overlays */
+
+ private var overlays = Document.Overlays.empty
+
+ override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+ synchronized { overlays(name) }
+
+ override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+ synchronized { overlays = overlays.insert(command, fn, args) }
+
+ override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+ synchronized { overlays = overlays.remove(command, fn, args) }
+
+
+ /* hyperlinks */
+
+ def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
+ {
+ Swing_Thread.require()
+
+ JEdit_Lib.jedit_buffer(file_name) match {
+ case Some(buffer) =>
+ view.goToBuffer(buffer)
+ val text_area = view.getTextArea
+
+ try {
+ val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
+ text_area.moveCaretPosition(line_start)
+ if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
+ }
+ catch {
+ case _: ArrayIndexOutOfBoundsException =>
+ case _: IllegalArgumentException =>
+ }
+
+ case None =>
+ val args =
+ if (line <= 0) Array(file_name)
+ else if (column <= 0) Array(file_name, "+line:" + line.toInt)
+ else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
+ jEdit.openFiles(view, null, args)
+ }
+ }
+
+ override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
+ new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
+
+ override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
+ : Option[Hyperlink] =
+ {
+ if (snapshot.is_outdated) None
+ else {
+ snapshot.state.find_command(snapshot.version, command.id) match {
+ case None => None
+ case Some((node, _)) =>
+ val file_name = command.node_name.node
+ val sources =
+ node.commands.iterator.takeWhile(_ != command).map(_.source) ++
+ (if (offset == 0) Iterator.empty
+ else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+ val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
+ Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
+ }
+ }
+ }
+}
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -30,7 +30,7 @@
private var zoom_factor = 100
private var do_update = true
- private var current_snapshot = Document.State.init.snapshot()
+ private var current_snapshot = Document.Snapshot.init
private var current_state = Command.empty.init_state
private var current_output: List[XML.Tree] = Nil
@@ -54,15 +54,14 @@
Swing_Thread.require()
val (new_snapshot, new_state) =
- Document_View(view.getTextArea) match {
- case Some(doc_view) =>
- val snapshot = doc_view.model.snapshot()
+ PIDE.editor.current_node_snapshot(view) match {
+ case Some(snapshot) =>
if (follow && !snapshot.is_outdated) {
- snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
- case Some(cmd) =>
+ PIDE.editor.current_command(view, snapshot) match {
+ case Some((cmd, _)) =>
(snapshot, snapshot.state.command_state(snapshot.version, cmd))
case None =>
- (Document.State.init.snapshot(), Command.empty.init_state)
+ (Document.Snapshot.init, Command.empty.init_state)
}
}
else (current_snapshot, current_state)
--- a/src/Tools/jEdit/src/plugin.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 12 18:02:01 2013 +0200
@@ -47,23 +47,11 @@
else Some(current_session.recent_syntax)
}
+ lazy val editor = new JEdit_Editor
+
/* document model and view */
- def document_snapshot(name: Document.Node.Name): Document.Snapshot =
- {
- Swing_Thread.require()
-
- JEdit_Lib.jedit_buffer(name.node) match {
- case Some(buffer) =>
- document_model(buffer) match {
- case Some(model) => model.snapshot
- case None => session.snapshot(name)
- }
- case None => session.snapshot(name)
- }
- }
-
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
@@ -95,7 +83,7 @@
thy_load.buffer_node_name(buffer) match {
case Some(node_name) =>
document_model(buffer) match {
- case Some(model) if model.name == node_name => (Nil, Some(model))
+ case Some(model) if model.node_name == node_name => (Nil, Some(model))
case _ =>
val model = Document_Model.init(session, buffer, node_name)
(model.init_edits(), Some(model))
@@ -131,23 +119,6 @@
Document_View.exit(text_area)
}
}
-
- def flush_buffers()
- {
- Swing_Thread.require()
-
- session.update(
- (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
- case (edits, buffer) =>
- JEdit_Lib.buffer_lock(buffer) {
- document_model(buffer) match {
- case Some(model) => model.flushed_edits() ::: edits
- case None => edits
- }
- }
- }
- )
- }
}
@@ -173,7 +144,7 @@
val thys =
for (buffer <- buffers; model <- PIDE.document_model(buffer))
- yield model.name
+ yield model.node_name
val thy_info = new Thy_Info(PIDE.thy_load)
// FIXME avoid I/O in Swing thread!?!
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 12 18:02:01 2013 +0200
@@ -64,7 +64,7 @@
private var current_font_family = "Dialog"
private var current_font_size: Int = 12
private var current_body: XML.Body = Nil
- private var current_base_snapshot = Document.State.init.snapshot()
+ private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
private var current_rendering: Rendering =
Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
--- a/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 15:48:57 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,226 +0,0 @@
-/* Title: Tools/jEdit/src/query_operation.scala
- Author: Makarius
-
-One-shot query operations via asynchronous print functions and temporary
-document overlays.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import scala.actors.Actor._
-
-import org.gjt.sp.jedit.View
-
-
-object Query_Operation
-{
- object Status extends Enumeration
- {
- val WAITING = Value("waiting")
- val RUNNING = Value("running")
- val FINISHED = Value("finished")
- }
-
- def apply(
- view: View,
- operation_name: String,
- consume_status: Status.Value => Unit,
- consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
- new Query_Operation(view, operation_name, consume_status, consume_output)
-}
-
-final class Query_Operation private(
- view: View,
- operation_name: String,
- consume_status: Query_Operation.Status.Value => Unit,
- consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit)
-{
- private val instance = Document_ID.make().toString
-
-
- /* implicit state -- owned by Swing thread */
-
- private var current_location: Option[Command] = None
- private var current_query: List[String] = Nil
- private var current_update_pending = false
- private var current_output: List[XML.Tree] = Nil
- private var current_status = Query_Operation.Status.FINISHED
- private var current_exec_id = Document_ID.none
-
- private def reset_state()
- {
- current_location = None
- current_query = Nil
- current_update_pending = false
- current_output = Nil
- current_status = Query_Operation.Status.FINISHED
- current_exec_id = Document_ID.none
- }
-
- private def remove_overlay()
- {
- Swing_Thread.require()
-
- for {
- command <- current_location
- buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
- model <- PIDE.document_model(buffer)
- } model.remove_overlay(command, operation_name, instance :: current_query)
- }
-
-
- /* content update */
-
- private def content_update()
- {
- Swing_Thread.require()
-
-
- /* snapshot */
-
- val (snapshot, state, removed) =
- current_location match {
- case Some(cmd) =>
- val snapshot = PIDE.document_snapshot(cmd.node_name)
- val state = snapshot.state.command_state(snapshot.version, cmd)
- val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
- (snapshot, state, removed)
- case None =>
- (Document.State.init.snapshot(), Command.empty.init_state, true)
- }
-
- val results =
- (for {
- (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
- if props.contains((Markup.INSTANCE, instance))
- } yield elem).toList
-
-
- /* output */
-
- val new_output =
- for {
- XML.Elem(_, List(XML.Elem(markup, body))) <- results
- if Markup.messages.contains(markup.name)
- } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)
-
-
- /* status */
-
- def get_status(name: String, status: Query_Operation.Status.Value)
- : Option[Query_Operation.Status.Value] =
- results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status })
-
- val new_status =
- if (removed) Query_Operation.Status.FINISHED
- else
- get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse
- get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse
- Query_Operation.Status.WAITING
-
- if (new_status == Query_Operation.Status.RUNNING)
- results.collectFirst(
- {
- case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem))
- if elem.name == Markup.RUNNING => id
- }).foreach(id => current_exec_id = id)
-
-
- /* state update */
-
- if (current_output != new_output || current_status != new_status) {
- if (snapshot.is_outdated)
- current_update_pending = true
- else {
- current_update_pending = false
- if (current_output != new_output && !removed) {
- current_output = new_output
- consume_output(snapshot, state.results, new_output)
- }
- if (current_status != new_status) {
- current_status = new_status
- consume_status(new_status)
- if (new_status == Query_Operation.Status.FINISHED) {
- remove_overlay()
- PIDE.flush_buffers()
- }
- }
- }
- }
- }
-
-
- /* query operations */
-
- def cancel_query(): Unit =
- Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) }
-
- def apply_query(query: List[String])
- {
- Swing_Thread.require()
-
- Document_View(view.getTextArea) match {
- case Some(doc_view) =>
- val snapshot = doc_view.model.snapshot()
- remove_overlay()
- reset_state()
- consume_output(Document.State.init.snapshot(), Command.Results.empty, Nil)
- snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
- case Some(command) =>
- current_location = Some(command)
- current_query = query
- current_status = Query_Operation.Status.WAITING
- doc_view.model.insert_overlay(command, operation_name, instance :: query)
- case None =>
- }
- consume_status(current_status)
- PIDE.flush_buffers()
- case None =>
- }
- }
-
- def locate_query()
- {
- Swing_Thread.require()
-
- current_location match {
- case Some(command) =>
- val snapshot = PIDE.document_snapshot(command.node_name)
- val commands = snapshot.node.commands
- if (commands.contains(command)) {
- // FIXME revert offset (!?)
- val sources = commands.iterator.takeWhile(_ != command).map(_.source)
- val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
- Hyperlink(command.node_name.node, line, column).follow(view)
- }
- case None =>
- }
- }
-
-
- /* main actor */
-
- private val main_actor = actor {
- loop {
- react {
- case changed: Session.Commands_Changed =>
- current_location match {
- case Some(command)
- if current_update_pending ||
- (current_status != Query_Operation.Status.FINISHED &&
- changed.commands.contains(command)) =>
- Swing_Thread.later { content_update() }
- case _ =>
- }
- case bad =>
- java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
- }
- }
- }
-
- def activate() { PIDE.session.commands_changed += main_actor }
- def deactivate() { PIDE.session.commands_changed -= main_actor }
-}
--- a/src/Tools/jEdit/src/rendering.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon Aug 12 18:02:01 2013 +0200
@@ -199,15 +199,16 @@
private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
- def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
+ def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
- snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ =>
+ snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
+ range, Nil, Some(hyperlink_include), _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
- val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
- Some(link :: links)
+ val link = PIDE.editor.hyperlink_file(jedit_file)
+ Some(Text.Info(snapshot.convert(info_range), link) :: links)
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
if !props.exists(
@@ -220,23 +221,16 @@
Isabelle_System.source_file(Path.explode(name)) match {
case Some(path) =>
val jedit_file = Isabelle_System.platform_path(path)
- val link =
- Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
- Some(link :: links)
+ val link = PIDE.editor.hyperlink_file(jedit_file, line)
+ Some(Text.Info(snapshot.convert(info_range), link) :: links)
case None => None
}
case Position.Def_Id_Offset(id, offset) =>
snapshot.state.find_command(snapshot.version, id) match {
case Some((node, command)) =>
- val sources =
- node.commands.iterator.takeWhile(_ != command).map(_.source) ++
- Iterator.single(command.source(Text.Range(0, command.decode(offset))))
- val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
- val link =
- Text.Info(snapshot.convert(info_range),
- Hyperlink(command.node_name.node, line, column))
- Some(link :: links)
+ PIDE.editor.hyperlink_command(snapshot, command, offset)
+ .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
case None => None
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 12 18:02:01 2013 +0200
@@ -135,7 +135,8 @@
private var control: Boolean = false
private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
- private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
+ private val hyperlink_area =
+ new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _)
private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
private val active_areas =
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -46,7 +46,7 @@
}
private val sledgehammer =
- Query_Operation(view, "sledgehammer", consume_status _,
+ new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
--- a/src/Tools/jEdit/src/text_overview.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Mon Aug 12 18:02:01 2013 +0200
@@ -53,7 +53,7 @@
private var cached_colors: List[(Color, Int, Int)] = Nil
- private var last_snapshot = Document.State.init.snapshot()
+ private var last_snapshot = Document.Snapshot.init
private var last_options = PIDE.options.value
private var last_relevant_range = Text.Range(0)
private var last_line_count = 0
--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -41,7 +41,7 @@
} model.node_required = !model.node_required
}
}
- else if (clicks == 2) Hyperlink(listData(index).node).follow(view)
+ else if (clicks == 2) PIDE.editor.goto(view, listData(index).node)
}
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
@@ -98,7 +98,7 @@
buffer <- JEdit_Lib.jedit_buffers
model <- PIDE.document_model(buffer)
if model.node_required
- } nodes_required += model.name
+ } nodes_required += model.node_name
}
update_nodes_required()
--- a/src/Tools/jEdit/src/timing_dockable.scala Mon Aug 12 15:48:57 2013 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Aug 12 18:02:01 2013 +0200
@@ -89,22 +89,14 @@
extends Entry
{
def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory)
- def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view)
+ def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) }
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
{
def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.name)
-
def follow(snapshot: Document.Snapshot)
- {
- val node = snapshot.version.nodes(command.node_name)
- if (node.commands.contains(command)) {
- val sources = node.commands.iterator.takeWhile(_ != command).map(_.source)
- val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
- Hyperlink(command.node_name.node, line, column).follow(view)
- }
- }
+ { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) }
}
@@ -165,7 +157,7 @@
val name =
Document_View(view.getTextArea) match {
case None => Document.Node.Name.empty
- case Some(doc_view) => doc_view.model.name
+ case Some(doc_view) => doc_view.model.node_name
}
val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)