--- a/NEWS Fri Feb 21 12:33:49 2014 +0100
+++ b/NEWS Fri Feb 21 17:06:48 2014 +0100
@@ -32,6 +32,11 @@
* Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
auxiliary ML files.
+* Improved completion based on context information about embedded
+languages: keywords are only completed for outer syntax, symbols for
+languages that support them. E.g. no symbol completion for ML source,
+but within ML strings, comments, antiquotations.
+
* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.
--- a/src/Pure/General/antiquote.ML Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/General/antiquote.ML Fri Feb 21 17:06:48 2014 +0100
@@ -32,7 +32,8 @@
(* reports *)
fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
- [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
+ [(start, Markup.antiquote), (stop, Markup.antiquote),
+ (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)];
fun antiquote_reports text =
maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
--- a/src/Pure/PIDE/command.scala Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/command.scala Fri Feb 21 17:06:48 2014 +0100
@@ -15,6 +15,8 @@
object Command
{
type Edit = (Option[Command], Option[Command])
+ type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
+
/** accumulated results from prover **/
@@ -54,21 +56,60 @@
}
+ /* markup */
+
+ object Markup_Index
+ {
+ val markup: Markup_Index = Markup_Index(false, "")
+ }
+
+ sealed case class Markup_Index(status: Boolean, file_name: String)
+
+ object Markups
+ {
+ val empty: Markups = new Markups(Map.empty)
+
+ def init(markup: Markup_Tree): Markups =
+ new Markups(Map(Markup_Index.markup -> markup))
+ }
+
+ final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
+ {
+ def apply(index: Markup_Index): Markup_Tree =
+ rep.getOrElse(index, Markup_Tree.empty)
+
+ def add(index: Markup_Index, markup: Text.Markup): Markups =
+ new Markups(rep + (index -> (this(index) + markup)))
+
+ def ++ (other: Markups): Markups =
+ new Markups(
+ (rep.keySet ++ other.rep.keySet)
+ .map(index => index -> (this(index) ++ other(index))).toMap)
+
+ override def hashCode: Int = rep.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Markups => rep == other.rep
+ case _ => false
+ }
+ override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
+ }
+
+
/* state */
sealed case class State(
command: Command,
status: List[Markup] = Nil,
results: Results = Results.empty,
- markups: Map[String, Markup_Tree] = Map.empty)
+ markups: Markups = Markups.empty)
{
- def get_markup(file_name: String): Markup_Tree =
- markups.getOrElse(file_name, Markup_Tree.empty)
+ /* markup */
- def markup: Markup_Tree = get_markup("")
+ def markup(index: Markup_Index): Markup_Tree = markups(index)
def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
- markup.to_XML(command.range, command.source, filter)
+ markup(Markup_Index.markup).to_XML(command.range, command.source, filter)
/* content */
@@ -79,10 +120,17 @@
results == other.results &&
markups == other.markups
- private def add_status(st: Markup): State = copy(status = st :: status)
+ private def add_status(st: Markup): State =
+ copy(status = st :: status)
- private def add_markup(file_name: String, m: Text.Markup): State =
- copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
+ private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
+ {
+ val markups1 =
+ if (status || Protocol.status_elements(m.info.name))
+ markups.add(Markup_Index(true, file_name), m)
+ else markups
+ copy(markups = markups1.add(Markup_Index(false, file_name), m))
+ }
def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
message match {
@@ -90,8 +138,9 @@
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
- state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
-
+ state.
+ add_status(markup).
+ add_markup(true, "", Text.Info(command.proper_range, elem))
case _ =>
System.err.println("Ignored status message: " + msg)
state
@@ -111,8 +160,8 @@
case Some(range) =>
if (!range.is_singularity) {
val props = Position.purge(atts)
- state.add_markup(file_name,
- Text.Info(range, XML.Elem(Markup(name, props), args)))
+ val info = Text.Info(range, XML.Elem(Markup(name, props), args))
+ state.add_markup(false, file_name, info)
}
else state
case None => bad(); state
@@ -125,7 +174,7 @@
val range = command.proper_range
val props = Position.purge(atts)
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup("", info)
+ state.add_markup(false, "", info)
case _ => /* FIXME bad(); */ state
}
@@ -141,7 +190,7 @@
for {
(file_name, chunk) <- command.chunks
range <- Protocol.message_positions(command.id, alt_id, chunk, message)
- } st = st.add_markup(file_name, Text.Info(range, message2))
+ } st = st.add_markup(false, file_name, Text.Info(range, message2))
}
st
@@ -155,9 +204,7 @@
copy(
status = other.status ::: status,
results = results ++ other.results,
- markups =
- (markups.keySet ++ other.markups.keySet)
- .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
+ markups = markups ++ other.markups
)
}
@@ -189,15 +236,7 @@
def name(span: List[Token]): String =
span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
- type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
-
- def apply(
- id: Document_ID.Command,
- node_name: Document.Node.Name,
- blobs: List[Blob],
- span: List[Token],
- results: Results = Results.empty,
- markup: Markup_Tree = Markup_Tree.empty): Command =
+ private def source_span(span: List[Token]): (String, List[Token]) =
{
val source: String =
span match {
@@ -213,16 +252,30 @@
span1 += Token(kind, s1)
i += n
}
-
- new Command(id, node_name, blobs, span1.toList, source, results, markup)
+ (source, span1.toList)
}
- val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+ def apply(
+ id: Document_ID.Command,
+ node_name: Document.Node.Name,
+ blobs: List[Blob],
+ span: List[Token]): Command =
+ {
+ val (source, span1) = source_span(span)
+ new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
+ }
- def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
- : Command =
- Command(id, Document.Node.Name.empty, Nil, List(Token(Token.Kind.UNPARSED, source)),
- results, markup)
+ val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+
+ def unparsed(
+ id: Document_ID.Command,
+ source: String,
+ results: Results,
+ markup: Markup_Tree): Command =
+ {
+ val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
+ new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
+ }
def unparsed(source: String): Command =
unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
@@ -316,7 +369,7 @@
/* accumulated results */
val init_state: Command.State =
- Command.State(this, results = init_results, markups = Map("" -> init_markup))
+ Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/document.scala Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/document.scala Fri Feb 21 17:06:48 2014 +0100
@@ -357,6 +357,7 @@
val state: State
val version: Version
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
@@ -366,15 +367,19 @@
val node: Node
val thy_load_commands: List[Command]
def eq_content(other: Snapshot): Boolean
- def cumulate_markup[A](
+
+ def cumulate[A](
range: Text.Range,
info: A,
elements: String => Boolean,
- result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
- def select_markup[A](
+ result: Command.State => (A, Text.Markup) => Option[A],
+ status: Boolean = false): List[Text.Info[A]]
+
+ def select[A](
range: Text.Range,
elements: String => Boolean,
- result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
+ result: Command.State => Text.Markup => Option[A],
+ status: Boolean = false): List[Text.Info[A]]
}
type Assign_Update =
@@ -601,14 +606,14 @@
val version = stable.version.get_finished
val is_outdated = !(pending_edits.isEmpty && latest == stable)
+
+ /* local node content */
+
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
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)
@@ -629,38 +634,51 @@
(thy_load_commands zip other.thy_load_commands).forall(eq_commands)
}
- def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
- result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
+
+ /* cumulate markup */
+
+ def cumulate[A](
+ range: Text.Range,
+ info: A,
+ elements: String => Boolean,
+ result: Command.State => (A, Text.Markup) => Option[A],
+ status: Boolean = false): List[Text.Info[A]] =
{
val former_range = revert(range)
thy_load_commands match {
case thy_load_command :: _ =>
val file_name = node_name.node
+ val markup_index = Command.Markup_Index(status, file_name)
(for {
chunk <- thy_load_command.chunks.get(file_name).iterator
st = state.command_state(version, thy_load_command)
res = result(st)
- Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
+ Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
former_range.restrict(chunk.range), info, elements,
{ case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
).iterator
} yield Text.Info(convert(r0), a)).toList
case _ =>
+ val markup_index = Command.Markup_Index(status, "")
(for {
(command, command_start) <- node.command_range(former_range)
st = state.command_state(version, command)
res = result(st)
- Text.Info(r0, a) <- st.markup.cumulate[A](
+ Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
(former_range - command_start).restrict(command.range), info, elements,
- { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
- ).iterator
+ {
+ case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
+ }).iterator
} yield Text.Info(convert(r0 + command_start), a)).toList
}
}
- def select_markup[A](range: Text.Range, elements: String => Boolean,
- result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
+ def select[A](
+ range: Text.Range,
+ elements: String => Boolean,
+ result: Command.State => Text.Markup => Option[A],
+ status: Boolean = false): List[Text.Info[A]] =
{
def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
{
@@ -671,7 +689,7 @@
case some => Some(some)
}
}
- for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
+ for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
yield Text.Info(r, x)
}
}
--- a/src/Pure/PIDE/markup.ML Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Feb 21 17:06:48 2014 +0100
@@ -28,6 +28,7 @@
val language_prop: T
val language_ML: T
val language_document: T
+ val language_antiquotation: T
val language_text: T
val language_rail: T
val bindingN: string val binding: T
@@ -255,9 +256,9 @@
val language_type = language "type" true;
val language_term = language "term" true;
val language_prop = language "prop" true;
-
val language_ML = language "ML" false;
val language_document = language "document" false;
+val language_antiquotation = language "antiquotation" true;
val language_text = language "text" true;
val language_rail = language "rail" true;
--- a/src/Pure/PIDE/markup_tree.scala Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Fri Feb 21 17:06:48 2014 +0100
@@ -38,53 +38,29 @@
/* tree building blocks */
- object Elements
- {
- val empty = new Elements(Set.empty)
- }
-
- final class Elements private(private val rep: Set[String])
- {
- def exists(pred: String => Boolean): Boolean = rep.exists(pred)
-
- def + (name: String): Elements =
- if (rep(name)) this
- else new Elements(rep + name)
-
- def + (elem: XML.Elem): Elements = this + elem.markup.name
- def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
-
- def ++ (other: Elements): Elements =
- if (this eq other) this
- else if (rep.isEmpty) other
- else (this /: other.rep)(_ + _)
- }
-
object Entry
{
def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
- Entry(markup.range, List(markup.info), Elements.empty + markup.info,
- subtree, subtree.make_elements)
-
- def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
- Entry(range, rev_markups, Elements.empty ++ rev_markups,
- subtree, subtree.make_elements)
+ Entry(markup.range, List(markup.info), subtree)
}
sealed case class Entry(
range: Text.Range,
rev_markup: List[XML.Elem],
- elements: Elements,
- subtree: Markup_Tree,
- subtree_elements: Elements)
+ subtree: Markup_Tree)
{
def markup: List[XML.Elem] = rev_markup.reverse
- def + (markup: Text.Markup): Entry =
- copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
+ def filter_markup(pred: String => Boolean): List[XML.Elem] =
+ {
+ var result: List[XML.Elem] = Nil
+ for { elem <- rev_markup; if (pred(elem.name)) }
+ result ::= elem
+ result.toList
+ }
- def \ (markup: Text.Markup): Entry =
- copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
+ def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
+ def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
}
object Branches
@@ -154,10 +130,6 @@
}
}
- def make_elements: Elements =
- (Elements.empty /: branches)(
- { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
-
def + (new_markup: Text.Markup): Markup_Tree =
{
val new_range = new_markup.range
@@ -230,8 +202,7 @@
var y = x
var changed = false
for {
- elem <- entry.markup
- if elements(elem.name)
+ elem <- entry.filter_markup(elements)
y1 <- result(y, Text.Info(entry.range, elem))
} { y = y1; changed = true }
if (changed) Some(y) else None
@@ -244,13 +215,10 @@
stack match {
case (parent, (range, entry) :: more) :: rest =>
val subrange = range.restrict(root_range)
- val subtree =
- if (entry.subtree_elements.exists(elements))
- entry.subtree.overlapping(subrange).toList
- else Nil
+ val subtree = entry.subtree.overlapping(subrange).toList
val start = subrange.start
- (if (entry.elements.exists(elements)) results(parent.info, entry) else None) match {
+ results(parent.info, entry) match {
case Some(res) =>
val next = Text.Info(subrange, res)
val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
--- a/src/Pure/PIDE/protocol.scala Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Feb 21 17:06:48 2014 +0100
@@ -63,10 +63,6 @@
def is_failed: Boolean = failed
}
- val command_status_markup: Set[String] =
- Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
- Markup.FINISHED, Markup.FAILED)
-
def command_status(status: Status, markup: Markup): Status =
markup match {
case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
@@ -81,6 +77,13 @@
def command_status(markups: List[Markup]): Status =
(Status.init /: markups)(command_status(_, _))
+ val command_status_elements: Set[String] =
+ Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+ Markup.FINISHED, Markup.FAILED)
+
+ val status_elements: Set[String] =
+ command_status_elements + Markup.WARNING + Markup.ERROR
+
/* command timing */
@@ -162,12 +165,12 @@
/* result messages */
- private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
+ private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
def clean_message(body: XML.Body): XML.Body =
body filter {
- case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
- case XML.Elem(Markup(name, _), _) => !clean(name)
+ case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
+ case XML.Elem(Markup(name, _), _) => !clean_elements(name)
case _ => true
} map {
case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
@@ -272,7 +275,8 @@
/* reported positions */
- private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+ private val position_elements =
+ Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(
command_id: Document_ID.Command,
@@ -294,9 +298,9 @@
def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
tree match {
case XML.Wrapped_Elem(Markup(name, props), _, body) =>
- body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+ body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
case XML.Elem(Markup(name, props), body) =>
- body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+ body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
case XML.Text(_) => set
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Feb 21 17:06:48 2014 +0100
@@ -159,9 +159,10 @@
case Some(snapshot) =>
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
- Isabelle_Sidekick.swing_markup_tree(
- snapshot.state.command_state(snapshot.version, command).markup, root,
- (info: Text.Info[List[XML.Elem]]) =>
+ val markup =
+ snapshot.state.command_state(snapshot.version, command).
+ markup(Command.Markup_Index.markup)
+ Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
--- a/src/Tools/jEdit/src/rendering.scala Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Fri Feb 21 17:06:48 2014 +0100
@@ -146,6 +146,75 @@
else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
else JEditToken.KEYWORD1
+
+
+ /* markup elements */
+
+ private val completion_elements =
+ Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
+ Markup.ML_STRING, Markup.ML_COMMENT)
+
+ private val highlight_elements =
+ Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
+ Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
+ Markup.VAR, Markup.TFREE, Markup.TVAR)
+
+ private val hyperlink_elements =
+ Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+
+ private val active_elements =
+ Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+ Markup.SENDBACK, Markup.SIMP_TRACE)
+
+ private val tooltip_message_elements =
+ Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+
+ private val tooltip_descriptions =
+ Map(
+ Markup.TOKEN_RANGE -> "inner syntax token",
+ Markup.FREE -> "free variable",
+ Markup.SKOLEM -> "skolem variable",
+ Markup.BOUND -> "bound variable",
+ Markup.VAR -> "schematic variable",
+ Markup.TFREE -> "free type variable",
+ Markup.TVAR -> "schematic type variable")
+
+ private val tooltip_elements =
+ Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+ Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
+ tooltip_descriptions.keys
+
+ private val gutter_elements =
+ Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
+ private val squiggly_elements =
+ Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
+ private val line_background_elements =
+ Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+ Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
+ Markup.INFORMATION)
+
+ private val separator_elements = Set(Markup.SEPARATOR)
+
+ private val background1_elements =
+ Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
+ Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
+ Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+ active_elements
+
+ private val background2_elements = Set(Markup.TOKEN_RANGE)
+
+ private val foreground_elements =
+ Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+ Markup.CARTOUCHE, Markup.ANTIQUOTED)
+
+ private val bullet_elements = Set(Markup.BULLET)
+
+ private val fold_depth_elements =
+ Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
}
@@ -202,14 +271,10 @@
/* completion context */
- private val completion_elements =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
- Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT)
-
def completion_context(caret: Text.Offset): Option[Completion.Context] =
if (caret > 0) {
val result =
- snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
+ snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
{
case Text.Info(_, elem)
if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
@@ -229,25 +294,22 @@
/* command status overview */
- val overview_limit = options.int("jedit_text_overview_limit")
-
- private val overview_elements =
- Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
+ def overview_limit: Int = options.int("jedit_text_overview_limit")
def overview_color(range: Text.Range): Option[Color] =
{
if (snapshot.is_outdated) None
else {
val results =
- snapshot.cumulate_markup[(Protocol.Status, Int)](
- range, (Protocol.Status.init, 0), overview_elements, _ =>
+ snapshot.cumulate[(Protocol.Status, Int)](
+ range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
{
case ((status, pri), Text.Info(_, elem)) =>
- if (Protocol.command_status_markup(elem.name))
+ if (Protocol.command_status_elements(elem.name))
Some((Protocol.command_status(status, elem.markup), pri))
else
Some((status, pri max Rendering.message_pri(elem.name)))
- })
+ }, status = true)
if (results.isEmpty) None
else {
val (status, pri) =
@@ -267,15 +329,9 @@
/* highlighted area */
- private val highlight_elements =
- Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
- Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
- Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
- Markup.VAR, Markup.TFREE, Markup.TVAR)
-
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
- snapshot.select_markup(range, highlight_elements, _ =>
+ snapshot.select(range, Rendering.highlight_elements, _ =>
{
case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
}) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
@@ -284,9 +340,6 @@
/* hyperlinks */
- private val hyperlink_elements =
- Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
-
private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
if (Path.is_ok(name))
Isabelle_System.source_file(Path.explode(name)).map(path =>
@@ -303,8 +356,8 @@
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
- snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
- range, Vector.empty, hyperlink_elements, _ =>
+ snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+ range, Vector.empty, Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
@@ -346,11 +399,8 @@
/* active elements */
- private val active_elements =
- Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
-
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
- snapshot.select_markup(range, active_elements, command_state =>
+ snapshot.select(range, Rendering.active_elements, command_state =>
{
case Text.Info(info_range, elem) =>
if (elem.name == Markup.DIALOG) {
@@ -368,7 +418,7 @@
def command_results(range: Text.Range): Command.Results =
{
val results =
- snapshot.select_markup[Command.Results](range, _ => true, command_state =>
+ snapshot.select[Command.Results](range, _ => true, command_state =>
{ case _ => Some(command_state.results) }).map(_.info)
(Command.Results.empty /: results)(_ ++ _)
}
@@ -376,14 +426,11 @@
/* tooltip messages */
- private val tooltip_message_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
-
def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
{
val results =
- snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
- range, Nil, tooltip_message_elements, _ =>
+ snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
+ range, Nil, Rendering.tooltip_message_elements, _ =>
{
case (msgs, Text.Info(info_range,
XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
@@ -410,25 +457,10 @@
/* tooltips */
- private val tooltips: Map[String, String] =
- Map(
- Markup.TOKEN_RANGE -> "inner syntax token",
- Markup.FREE -> "free variable",
- Markup.SKOLEM -> "skolem variable",
- Markup.BOUND -> "bound variable",
- Markup.VAR -> "schematic variable",
- Markup.TFREE -> "free type variable",
- Markup.TVAR -> "schematic type variable")
-
- private val tooltip_elements =
- Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
- Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
- tooltips.keys
-
private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
- private val timing_threshold: Double = options.real("jedit_timing_threshold")
+ private def timing_threshold: Double = options.real("jedit_timing_threshold")
def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
{
@@ -443,8 +475,8 @@
}
val results =
- snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
- range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
+ snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
+ range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
{
case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
Some(Text.Info(r, (t1 + t2, info)))
@@ -471,9 +503,8 @@
case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
Some(add(prev, r, (true, XML.Text("language: " + language))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
- if (tooltips.isDefinedAt(name))
- Some(add(prev, r, (true, XML.Text(tooltips(name)))))
- else None
+ Rendering.tooltip_descriptions.get(name).
+ map(descr => add(prev, r, (true, XML.Text(descr))))
}).map(_.info)
results.map(_.info).flatMap(res => res._2.toList) match {
@@ -485,7 +516,7 @@
}
}
- val tooltip_margin: Int = options.int("jedit_tooltip_margin")
+ def tooltip_margin: Int = options.int("jedit_tooltip_margin")
lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
@@ -499,13 +530,10 @@
Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
- private val gutter_elements =
- Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
-
def gutter_message(range: Text.Range): Option[Icon] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
+ snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
@@ -528,18 +556,16 @@
/* squiggly underline */
- private val squiggly_colors = Map(
+ private lazy val squiggly_colors = Map(
Rendering.writeln_pri -> writeln_color,
Rendering.information_pri -> information_color,
Rendering.warning_pri -> warning_color,
Rendering.error_pri -> error_color)
- private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
-
def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
+ snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
{
case (pri, Text.Info(_, elem)) =>
if (Protocol.is_information(elem))
@@ -556,21 +582,17 @@
/* message output */
- private val message_colors = Map(
+ private lazy val message_colors = Map(
Rendering.writeln_pri -> writeln_message_color,
Rendering.information_pri -> information_message_color,
Rendering.tracing_pri -> tracing_message_color,
Rendering.warning_pri -> warning_message_color,
Rendering.error_pri -> error_message_color)
- private val line_background_elements =
- Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
- Markup.ERROR_MESSAGE, Markup.INFORMATION)
-
def line_background(range: Text.Range): Option[(Color, Boolean)] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
+ snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
{
case (pri, Text.Info(_, elem)) =>
if (elem.name == Markup.INFORMATION)
@@ -582,7 +604,7 @@
val is_separator =
pri > 0 &&
- snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
+ snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
{
case _ => Some(true)
}).exists(_.info)
@@ -596,38 +618,34 @@
/* text background */
- private val background1_elements =
- Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
- Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
- active_elements
-
def background1(range: Text.Range): List[Text.Info[Color]] =
{
if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
else
for {
Text.Info(r, result) <-
- snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
- range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
- {
- case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
- if (Protocol.command_status_markup(markup.name)) =>
- Some((Some(Protocol.command_status(status, markup)), color))
- case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
- Some((None, Some(bad_color)))
- case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
- Some((None, Some(intensify_color)))
- case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
- command_state.results.get(serial) match {
- case Some(Protocol.Dialog_Result(res)) if res == result =>
- Some((None, Some(active_result_color)))
- case _ =>
- Some((None, Some(active_color)))
- }
- case (_, Text.Info(_, elem)) =>
- if (active_elements(elem.name)) Some((None, Some(active_color)))
- else None
- })
+ snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
+ range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
+ command_state =>
+ {
+ case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+ if (Protocol.command_status_elements(markup.name)) =>
+ Some((Some(Protocol.command_status(status, markup)), color))
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
+ Some((None, Some(bad_color)))
+ case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
+ Some((None, Some(intensify_color)))
+ case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+ command_state.results.get(serial) match {
+ case Some(Protocol.Dialog_Result(res)) if res == result =>
+ Some((None, Some(active_result_color)))
+ case _ =>
+ Some((None, Some(active_color)))
+ }
+ case (_, Text.Info(_, elem)) =>
+ if (Rendering.active_elements(elem.name)) Some((None, Some(active_color)))
+ else None
+ })
color <-
(result match {
case (Some(status), opt_color) =>
@@ -640,16 +658,13 @@
}
def background2(range: Text.Range): List[Text.Info[Color]] =
- snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
+ snapshot.select(range, Rendering.background2_elements, _ => _ => Some(light_color))
/* text foreground */
- private val foreground_elements =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
-
def foreground(range: Text.Range): List[Text.Info[Color]] =
- snapshot.select_markup(range, foreground_elements, _ =>
+ snapshot.select(range, Rendering.foreground_elements, _ =>
{
case Text.Info(_, elem) =>
if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
@@ -658,7 +673,7 @@
/* text color */
- private val text_colors: Map[String, Color] = Map(
+ private lazy val text_colors: Map[String, Color] = Map(
Markup.KEYWORD1 -> keyword1_color,
Markup.KEYWORD2 -> keyword2_color,
Markup.STRING -> Color.BLACK,
@@ -687,13 +702,13 @@
Markup.ML_STRING -> inner_quoted_color,
Markup.ML_COMMENT -> inner_comment_color)
- private val text_color_elements = text_colors.keySet
+ private lazy val text_color_elements = text_colors.keySet
def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
{
if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
else
- snapshot.cumulate_markup(range, color, text_color_elements, _ =>
+ snapshot.cumulate(range, color, text_color_elements, _ =>
{
case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
})
@@ -703,16 +718,13 @@
/* virtual bullets */
def bullet(range: Text.Range): List[Text.Info[Color]] =
- snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
+ snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
/* text folds */
- private val fold_depth_elements =
- Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
-
def fold_depth(range: Text.Range): List[Text.Info[Int]] =
- snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
+ snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ =>
{
case (depth, _) => Some(depth + 1)
})