--- a/src/Pure/PIDE/command.scala Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Aug 02 14:26:09 2013 +0200
@@ -14,6 +14,9 @@
object Command
{
+ type Edit = (Option[Command], Option[Command])
+
+
/** accumulated results from prover **/
/* results */
--- a/src/Pure/PIDE/document.ML Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Aug 02 14:26:09 2013 +0200
@@ -9,11 +9,12 @@
sig
val timing: bool Unsynchronized.ref
type node_header = string * Thy_Header.header * string list
+ type overlay = Document_ID.command * string * string list
datatype node_edit =
Clear | (* FIXME unused !? *)
Edits of (Document_ID.command option * Document_ID.command option) list |
Deps of node_header |
- Perspective of bool * Document_ID.command list
+ Perspective of bool * Document_ID.command list * overlay list
type edit = string * node_edit
type state
val init_state: state
@@ -40,12 +41,18 @@
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
type node_header = string * Thy_Header.header * string list;
-type perspective = bool * Inttab.set * Document_ID.command option;
+
+type perspective =
+ {required: bool, (*required node*)
+ visible: Inttab.set, (*visible commands*)
+ visible_last: Document_ID.command option, (*last visible command*)
+ overlays: (string * string list) list Inttab.table}; (*command id -> print function with args*)
+
structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
- perspective: perspective, (*required node, visible commands, last visible command*)
+ perspective: perspective, (*command perspective*)
entries: Command.exec option Entries.T, (*command entries with excecutions*)
result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
@@ -57,11 +64,14 @@
fun map_node f (Node {header, perspective, entries, result}) =
make_node (f (header, perspective, entries, result));
-fun make_perspective (required, command_ids) : perspective =
- (required, Inttab.make_set command_ids, try List.last command_ids);
+fun make_perspective (required, command_ids, overlays) : perspective =
+ {required = required,
+ visible = Inttab.make_set command_ids,
+ visible_last = try List.last command_ids,
+ overlays = Inttab.make_list (map (fn (x, y, z) => (x, (y, z))) overlays)};
val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
-val no_perspective = make_perspective (false, []);
+val no_perspective = make_perspective (false, [], []);
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
@@ -86,10 +96,11 @@
fun set_perspective args =
map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
-val required_node = #1 o get_perspective;
-val visible_command = Inttab.defined o #2 o get_perspective;
-val visible_last = #3 o get_perspective;
+val required_node = #required o get_perspective;
+val visible_command = Inttab.defined o #visible o get_perspective;
+val visible_last = #visible_last o get_perspective;
val visible_node = is_some o visible_last
+val overlays = #overlays o get_perspective;
fun map_entries f =
map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
@@ -124,11 +135,13 @@
(* node edits and associated executions *)
+type overlay = Document_ID.command * string * string list;
+
datatype node_edit =
Clear |
Edits of (Document_ID.command option * Document_ID.command option) list |
Deps of node_header |
- Perspective of bool * Document_ID.command list;
+ Perspective of bool * Document_ID.command list * overlay list;
type edit = string * node_edit;
--- a/src/Pure/PIDE/document.scala Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/document.scala Fri Aug 02 14:26:09 2013 +0200
@@ -15,11 +15,28 @@
{
/** document structure **/
+ /* overlays -- print functions with arguments */
+
+ type Overlay = (Command, String, List[String])
+
+ object Overlays
+ {
+ val empty = new Overlays(Set.empty)
+ }
+
+ final class Overlays private(rep: Set[Overlay])
+ {
+ def + (o: Overlay) = new Overlays(rep + o)
+ def - (o: Overlay) = new Overlays(rep - o)
+ def dest: List[Overlay] = rep.toList
+ }
+
+
/* individual nodes */
type Edit[A, B] = (Node.Name, Node.Edit[A, B])
type Edit_Text = Edit[Text.Edit, Text.Perspective]
- type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
+ type Edit_Command = Edit[Command.Edit, Command.Perspective]
object Node
{
@@ -66,8 +83,9 @@
case class Clear[A, B]() extends Edit[A, B]
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
case class Deps[A, B](header: Header) extends Edit[A, B]
- case class Perspective[A, B](required: Boolean, perspective: B) extends Edit[A, B]
+ case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
+ type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
@@ -87,7 +105,8 @@
final class Node private(
val header: Node.Header = Node.bad_header("Bad theory header"),
- val perspective: (Boolean, Command.Perspective) = (false, Command.Perspective.empty),
+ val perspective: Node.Perspective_Command =
+ Node.Perspective(false, Command.Perspective.empty, Overlays.empty),
val commands: Linear_Set[Command] = Linear_Set.empty)
{
def clear: Node = new Node(header = header)
@@ -95,11 +114,13 @@
def update_header(new_header: Node.Header): Node =
new Node(new_header, perspective, commands)
- def update_perspective(new_perspective: (Boolean, Command.Perspective)): Node =
+ def update_perspective(new_perspective: Node.Perspective_Command): Node =
new Node(header, new_perspective, commands)
- def same_perspective(other: (Boolean, Command.Perspective)): Boolean =
- perspective._1 == other._1 && (perspective._2 same other._2)
+ def same_perspective(other_perspective: Node.Perspective_Command): Boolean =
+ perspective.required == other_perspective.required &&
+ perspective.visible.same(other_perspective.visible) &&
+ perspective.overlays == other_perspective.overlays
def update_commands(new_commands: Linear_Set[Command]): Node =
new Node(header, perspective, new_commands)
--- a/src/Pure/PIDE/protocol.ML Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Aug 02 14:26:09 2013 +0200
@@ -56,7 +56,9 @@
val imports' = map (rpair Position.none) imports;
val header = Thy_Header.make (name, Position.none) imports' keywords;
in Document.Deps (master, header, errors) end,
- fn (a :: b, []) => Document.Perspective (bool_atom a, map int_atom b)]))
+ fn (a :: b, c) =>
+ Document.Perspective (bool_atom a, map int_atom b,
+ list (triple int string (list string)) c)]))
end;
val (removed, assign_update, state') = Document.update old_id new_id edits state;
--- a/src/Pure/PIDE/protocol.scala Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Aug 02 14:26:09 2013 +0200
@@ -326,7 +326,7 @@
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
def encode_edit(name: Document.Node.Name)
- : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
+ : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) }, // FIXME unused !?
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
@@ -340,8 +340,9 @@
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
list(Encode.string)))))(
(dir, (name.theory, (imports, (keywords, header.errors)))))) },
- { case Document.Node.Perspective(a, b) =>
- (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) }))
+ { case Document.Node.Perspective(a, b, c) =>
+ (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
+ list(triple(id, Encode.string, list(Encode.string)))(c.dest)) }))
def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
val (name, edit) = node_edit
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 02 14:26:09 2013 +0200
@@ -293,7 +293,7 @@
/* main */
def diff_commands(old_cmds: Linear_Set[Command], new_cmds: Linear_Set[Command])
- : List[(Option[Command], Option[Command])] =
+ : List[Command.Edit] =
{
val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
@@ -311,17 +311,18 @@
case (name, Document.Node.Edits(text_edits)) =>
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
- val commands2 = recover_spans(syntax, name, node.perspective._2, commands1)
+ val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
node.update_commands(commands2)
case (_, Document.Node.Deps(_)) => node
- case (name, Document.Node.Perspective(required, text_perspective)) =>
- val perspective = (required, command_perspective(node, text_perspective))
+ case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
+ val perspective: Document.Node.Perspective_Command =
+ Document.Node.Perspective(required, command_perspective(node, text_perspective), overlays)
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(syntax, reparse_limit, name, perspective._2, node.commands))
+ consolidate_spans(syntax, reparse_limit, name, perspective.visible, node.commands))
}
}
@@ -354,8 +355,7 @@
val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
if (!(node.same_perspective(node2.perspective)))
- doc_edits +=
- (name -> Document.Node.Perspective(node2.perspective._1, node2.perspective._2))
+ doc_edits += (name -> node2.perspective)
doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
--- a/src/Tools/jEdit/src/document_model.scala Fri Aug 02 12:19:29 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Aug 02 14:26:09 2013 +0200
@@ -77,8 +77,28 @@
}
+ /* overlays */
+
+ private var overlays = Document.Overlays.empty
+
+ def add_overlay(command: Command, name: String, args: List[String])
+ {
+ Swing_Thread.required()
+ overlays += ((command, name, args))
+ PIDE.flush_buffers()
+ }
+
+ def remove_overlay(command: Command, name: String, args: List[String])
+ {
+ Swing_Thread.required()
+ overlays -= ((command, name, args))
+ PIDE.flush_buffers()
+ }
+
+
/* perspective */
+ // owned by Swing thread
private var _node_required = false
def node_required: Boolean = _node_required
def node_required_=(b: Boolean)
@@ -91,21 +111,21 @@
}
}
+ val empty_perspective: Document.Node.Perspective_Text =
+ Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
+
def node_perspective(): Document.Node.Perspective_Text =
{
Swing_Thread.require()
- val perspective =
- if (Isabelle.continuous_checking) {
- (node_required, Text.Perspective(
- for {
- doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective().ranges
- } yield range))
- }
- else (false, Text.Perspective.empty)
-
- Document.Node.Perspective(perspective._1, perspective._2)
+ if (Isabelle.continuous_checking) {
+ Document.Node.Perspective(node_required, Text.Perspective(
+ for {
+ doc_view <- PIDE.document_views(buffer)
+ range <- doc_view.perspective().ranges
+ } yield range), overlays)
+ }
+ else empty_perspective
}
@@ -143,8 +163,7 @@
private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
- private var last_perspective: Document.Node.Perspective_Text =
- Document.Node.Perspective(node_required, Text.Perspective.empty)
+ private var last_perspective = empty_perspective
def snapshot(): List[Text.Edit] = pending.toList