renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Nov 28 20:31:53 2011 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Nov 28 20:39:08 2011 +0100
@@ -14,8 +14,8 @@
"src/html_panel.scala"
"src/isabelle_encoding.scala"
"src/isabelle_hyperlinks.scala"
- "src/isabelle_markup.scala"
"src/isabelle_options.scala"
+ "src/isabelle_rendering.scala"
"src/isabelle_sidekick.scala"
"src/jedit_thy_load.scala"
"src/output_dockable.scala"
--- a/src/Tools/jEdit/src/document_view.scala Mon Nov 28 20:31:53 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Mon Nov 28 20:39:08 2011 +0100
@@ -193,7 +193,7 @@
val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
// FIXME snapshot.cumulate
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.popup) match {
case Text.Info(_, Some(msg)) #:: _ =>
val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
html_panel.render_sync(List(msg))
@@ -212,7 +212,7 @@
: Option[(Text.Range, Color)] =
{
val offset = text_area.xyToOffset(x, y)
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.subexp) match {
case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
case _ => None
}
@@ -279,12 +279,12 @@
if (control) {
val tooltips =
- (snapshot.select_markup(range)(Isabelle_Markup.tooltip1) match
+ (snapshot.select_markup(range)(Isabelle_Rendering.tooltip1) match
{
case Text.Info(_, Some(text)) #:: _ => List(text)
case _ => Nil
}) :::
- (snapshot.select_markup(range)(Isabelle_Markup.tooltip2) match
+ (snapshot.select_markup(range)(Isabelle_Rendering.tooltip2) match
{
case Text.Info(_, Some(text)) #:: _ => List(text)
case _ => Nil
@@ -293,7 +293,7 @@
else Isabelle.tooltip(tooltips.mkString("\n"))
}
else {
- snapshot.cumulate_markup(range)(Isabelle_Markup.tooltip_message) match
+ snapshot.cumulate_markup(range)(Isabelle_Rendering.tooltip_message) match
{
case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
@@ -326,7 +326,7 @@
// gutter icons
val icons =
(for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
- snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
+ snapshot.select_markup(line_range)(Isabelle_Rendering.gutter_message).iterator)
yield icon).toList.sortWith(_ >= _)
icons match {
case icon :: _ =>
@@ -432,7 +432,7 @@
(line1, line2) <- line_range(command, start)
val y = line_to_y(line1)
val height = HEIGHT * (line2 - line1)
- color <- Isabelle_Markup.overview_color(snapshot, command)
+ color <- Isabelle_Rendering.overview_color(snapshot, command)
} {
gfx.setColor(color)
gfx.fillRect(0, y, getWidth - 1, height)
--- a/src/Tools/jEdit/src/isabelle_markup.scala Mon Nov 28 20:31:53 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-/* Title: Tools/jEdit/src/isabelle_markup.scala
- Author: Makarius
-
-Isabelle specific physical rendering and markup selection.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.Color
-
-import org.lobobrowser.util.gui.ColorFactory
-import org.gjt.sp.jedit.syntax.{Token => JEditToken}
-
-import scala.collection.immutable.SortedMap
-
-
-object Isabelle_Markup
-{
- /* physical rendering */
-
- // see http://www.w3schools.com/css/css_colornames.asp
-
- def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
-
- val outdated_color = new Color(238, 227, 227)
- val running_color = new Color(97, 0, 97)
- val running1_color = new Color(97, 0, 97, 100)
- val unprocessed_color = new Color(255, 160, 160)
- val unprocessed1_color = new Color(255, 160, 160, 50)
-
- val light_color = new Color(240, 240, 240)
- val regular_color = new Color(192, 192, 192)
- val warning_color = new Color(255, 140, 0)
- val error_color = new Color(178, 34, 34)
- val error1_color = new Color(178, 34, 34, 50)
- val bad_color = new Color(255, 106, 106, 100)
- val hilite_color = new Color(255, 204, 102, 100)
-
- val quoted_color = new Color(139, 139, 139, 25)
- val subexp_color = new Color(80, 80, 80, 50)
-
- val keyword1_color = get_color("#006699")
- val keyword2_color = get_color("#009966")
-
- class Icon(val priority: Int, val icon: javax.swing.Icon)
- {
- def >= (that: Icon): Boolean = this.priority >= that.priority
- }
- val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
- val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
- val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
-
-
- /* command status */
-
- def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
- {
- val state = snapshot.command_state(command)
- if (snapshot.is_outdated) Some(outdated_color)
- else
- Isar_Document.command_status(state.status) match {
- case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
- case Isar_Document.Unprocessed => Some(unprocessed1_color)
- case _ => None
- }
- }
-
- def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
- {
- val state = snapshot.command_state(command)
- if (snapshot.is_outdated) None
- else
- Isar_Document.command_status(state.status) match {
- case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
- case Isar_Document.Unprocessed => Some(unprocessed_color)
- case Isar_Document.Failed => Some(error_color)
- case Isar_Document.Finished =>
- if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
- else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
- else None
- }
- }
-
-
- /* markup selectors */
-
- val message =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
- },
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
-
- val tooltip_message =
- Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
- {
- case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
- if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
- msgs + (serial ->
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
- },
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
-
- val gutter_message =
- Markup_Tree.Select[Icon](
- {
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
- body match {
- case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
- case _ => warning_icon
- }
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
- },
- Some(Set(Markup.WARNING, Markup.ERROR)))
-
- val background1 =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
- case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
- },
- Some(Set(Markup.BAD, Markup.HILITE)))
-
- val background2 =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
- },
- Some(Set(Markup.TOKEN_RANGE)))
-
- val foreground =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
- },
- Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
-
- private val text_colors: Map[String, Color] =
- Map(
- Markup.STRING -> get_color("black"),
- Markup.ALTSTRING -> get_color("black"),
- Markup.VERBATIM -> get_color("black"),
- Markup.LITERAL -> keyword1_color,
- Markup.DELIMITER -> get_color("black"),
- Markup.TFREE -> get_color("#A020F0"),
- Markup.TVAR -> get_color("#A020F0"),
- Markup.FREE -> get_color("blue"),
- Markup.SKOLEM -> get_color("#D2691E"),
- Markup.BOUND -> get_color("green"),
- Markup.VAR -> get_color("#00009B"),
- Markup.INNER_STRING -> get_color("#D2691E"),
- Markup.INNER_COMMENT -> get_color("#8B0000"),
- Markup.DYNAMIC_FACT -> get_color("#7BA428"),
- Markup.ML_KEYWORD -> keyword1_color,
- Markup.ML_DELIMITER -> get_color("black"),
- Markup.ML_NUMERAL -> get_color("red"),
- Markup.ML_CHAR -> get_color("#D2691E"),
- Markup.ML_STRING -> get_color("#D2691E"),
- Markup.ML_COMMENT -> get_color("#8B0000"),
- Markup.ML_MALFORMED -> get_color("#FF6A6A"),
- Markup.ANTIQ -> get_color("blue"))
-
- val text_color =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(m, _), _))
- if text_colors.isDefinedAt(m) => text_colors(m)
- },
- Some(Set() ++ text_colors.keys))
-
- private val tooltips: Map[String, String] =
- Map(
- Markup.SORT -> "sort",
- Markup.TYP -> "type",
- Markup.TERM -> "term",
- Markup.PROP -> "proposition",
- 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",
- Markup.ML_SOURCE -> "ML source",
- Markup.DOC_SOURCE -> "document source")
-
- private def string_of_typing(kind: String, body: XML.Body): String =
- Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
- margin = Isabelle.Int_Property("tooltip-margin"))
-
- val tooltip1 =
- Markup_Tree.Select[String](
- {
- case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
- case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- string_of_typing("ML:", body)
- case Text.Info(_, XML.Elem(Markup(name, _), _))
- if tooltips.isDefinedAt(name) => tooltips(name)
- },
- Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
-
- val tooltip2 =
- Markup_Tree.Select[String](
- {
- case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
- },
- Some(Set(Markup.TYPING)))
-
- private val subexp_include =
- Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
- Markup.ENTITY, Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
- Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
-
- val subexp =
- Markup_Tree.Select[(Text.Range, Color)](
- {
- case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
- (range, subexp_color)
- },
- Some(subexp_include))
-
-
- /* token markup -- text styles */
-
- private val command_style: Map[String, Byte] =
- {
- import JEditToken._
- Map[String, Byte](
- Keyword.THY_END -> KEYWORD2,
- Keyword.THY_SCRIPT -> LABEL,
- Keyword.PRF_SCRIPT -> LABEL,
- Keyword.PRF_ASM -> KEYWORD3,
- Keyword.PRF_ASM_GOAL -> KEYWORD3
- ).withDefaultValue(KEYWORD1)
- }
-
- private val token_style: Map[Token.Kind.Value, Byte] =
- {
- import JEditToken._
- Map[Token.Kind.Value, Byte](
- Token.Kind.KEYWORD -> KEYWORD2,
- Token.Kind.IDENT -> NULL,
- Token.Kind.LONG_IDENT -> NULL,
- Token.Kind.SYM_IDENT -> NULL,
- Token.Kind.VAR -> NULL,
- Token.Kind.TYPE_IDENT -> NULL,
- Token.Kind.TYPE_VAR -> NULL,
- Token.Kind.NAT -> NULL,
- Token.Kind.FLOAT -> NULL,
- Token.Kind.STRING -> LITERAL1,
- Token.Kind.ALT_STRING -> LITERAL2,
- Token.Kind.VERBATIM -> COMMENT3,
- Token.Kind.SPACE -> NULL,
- Token.Kind.COMMENT -> COMMENT1,
- Token.Kind.UNPARSED -> INVALID
- ).withDefaultValue(NULL)
- }
-
- def token_markup(syntax: Outer_Syntax, token: Token): Byte =
- if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
- else if (token.is_operator) JEditToken.OPERATOR
- else token_style(token.kind)
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Nov 28 20:39:08 2011 +0100
@@ -0,0 +1,270 @@
+/* Title: Tools/jEdit/src/isabelle_rendering.scala
+ Author: Makarius
+
+Isabelle specific physical rendering and markup selection.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Color
+
+import org.lobobrowser.util.gui.ColorFactory
+import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+
+import scala.collection.immutable.SortedMap
+
+
+object Isabelle_Rendering
+{
+ /* physical rendering */
+
+ // see http://www.w3schools.com/css/css_colornames.asp
+
+ def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
+
+ val outdated_color = new Color(238, 227, 227)
+ val running_color = new Color(97, 0, 97)
+ val running1_color = new Color(97, 0, 97, 100)
+ val unprocessed_color = new Color(255, 160, 160)
+ val unprocessed1_color = new Color(255, 160, 160, 50)
+
+ val light_color = new Color(240, 240, 240)
+ val regular_color = new Color(192, 192, 192)
+ val warning_color = new Color(255, 140, 0)
+ val error_color = new Color(178, 34, 34)
+ val error1_color = new Color(178, 34, 34, 50)
+ val bad_color = new Color(255, 106, 106, 100)
+ val hilite_color = new Color(255, 204, 102, 100)
+
+ val quoted_color = new Color(139, 139, 139, 25)
+ val subexp_color = new Color(80, 80, 80, 50)
+
+ val keyword1_color = get_color("#006699")
+ val keyword2_color = get_color("#009966")
+
+ class Icon(val priority: Int, val icon: javax.swing.Icon)
+ {
+ def >= (that: Icon): Boolean = this.priority >= that.priority
+ }
+ val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
+ val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
+ val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
+
+
+ /* command status */
+
+ def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ {
+ val state = snapshot.command_state(command)
+ if (snapshot.is_outdated) Some(outdated_color)
+ else
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
+ case Isar_Document.Unprocessed => Some(unprocessed1_color)
+ case _ => None
+ }
+ }
+
+ def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ {
+ val state = snapshot.command_state(command)
+ if (snapshot.is_outdated) None
+ else
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
+ case Isar_Document.Unprocessed => Some(unprocessed_color)
+ case Isar_Document.Failed => Some(error_color)
+ case Isar_Document.Finished =>
+ if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
+ else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
+ else None
+ }
+ }
+
+
+ /* markup selectors */
+
+ val message =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+ },
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
+
+ val tooltip_message =
+ Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
+ {
+ case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
+ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+ msgs + (serial ->
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+ },
+ Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
+
+ val gutter_message =
+ Markup_Tree.Select[Icon](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+ body match {
+ case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+ case _ => warning_icon
+ }
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+ },
+ Some(Set(Markup.WARNING, Markup.ERROR)))
+
+ val background1 =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+ case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
+ },
+ Some(Set(Markup.BAD, Markup.HILITE)))
+
+ val background2 =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+ },
+ Some(Set(Markup.TOKEN_RANGE)))
+
+ val foreground =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+ },
+ Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
+
+ private val text_colors: Map[String, Color] =
+ Map(
+ Markup.STRING -> get_color("black"),
+ Markup.ALTSTRING -> get_color("black"),
+ Markup.VERBATIM -> get_color("black"),
+ Markup.LITERAL -> keyword1_color,
+ Markup.DELIMITER -> get_color("black"),
+ Markup.TFREE -> get_color("#A020F0"),
+ Markup.TVAR -> get_color("#A020F0"),
+ Markup.FREE -> get_color("blue"),
+ Markup.SKOLEM -> get_color("#D2691E"),
+ Markup.BOUND -> get_color("green"),
+ Markup.VAR -> get_color("#00009B"),
+ Markup.INNER_STRING -> get_color("#D2691E"),
+ Markup.INNER_COMMENT -> get_color("#8B0000"),
+ Markup.DYNAMIC_FACT -> get_color("#7BA428"),
+ Markup.ML_KEYWORD -> keyword1_color,
+ Markup.ML_DELIMITER -> get_color("black"),
+ Markup.ML_NUMERAL -> get_color("red"),
+ Markup.ML_CHAR -> get_color("#D2691E"),
+ Markup.ML_STRING -> get_color("#D2691E"),
+ Markup.ML_COMMENT -> get_color("#8B0000"),
+ Markup.ML_MALFORMED -> get_color("#FF6A6A"),
+ Markup.ANTIQ -> get_color("blue"))
+
+ val text_color =
+ Markup_Tree.Select[Color](
+ {
+ case Text.Info(_, XML.Elem(Markup(m, _), _))
+ if text_colors.isDefinedAt(m) => text_colors(m)
+ },
+ Some(Set() ++ text_colors.keys))
+
+ private val tooltips: Map[String, String] =
+ Map(
+ Markup.SORT -> "sort",
+ Markup.TYP -> "type",
+ Markup.TERM -> "term",
+ Markup.PROP -> "proposition",
+ 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",
+ Markup.ML_SOURCE -> "ML source",
+ Markup.DOC_SOURCE -> "document source")
+
+ private def string_of_typing(kind: String, body: XML.Body): String =
+ Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
+ margin = Isabelle.Int_Property("tooltip-margin"))
+
+ val tooltip1 =
+ Markup_Tree.Select[String](
+ {
+ case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
+ case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+ string_of_typing("ML:", body)
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if tooltips.isDefinedAt(name) => tooltips(name)
+ },
+ Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
+
+ val tooltip2 =
+ Markup_Tree.Select[String](
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+ },
+ Some(Set(Markup.TYPING)))
+
+ private val subexp_include =
+ Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Markup.ENTITY, Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
+ Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
+
+ val subexp =
+ Markup_Tree.Select[(Text.Range, Color)](
+ {
+ case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ (range, subexp_color)
+ },
+ Some(subexp_include))
+
+
+ /* token markup -- text styles */
+
+ private val command_style: Map[String, Byte] =
+ {
+ import JEditToken._
+ Map[String, Byte](
+ Keyword.THY_END -> KEYWORD2,
+ Keyword.THY_SCRIPT -> LABEL,
+ Keyword.PRF_SCRIPT -> LABEL,
+ Keyword.PRF_ASM -> KEYWORD3,
+ Keyword.PRF_ASM_GOAL -> KEYWORD3
+ ).withDefaultValue(KEYWORD1)
+ }
+
+ private val token_style: Map[Token.Kind.Value, Byte] =
+ {
+ import JEditToken._
+ Map[Token.Kind.Value, Byte](
+ Token.Kind.KEYWORD -> KEYWORD2,
+ Token.Kind.IDENT -> NULL,
+ Token.Kind.LONG_IDENT -> NULL,
+ Token.Kind.SYM_IDENT -> NULL,
+ Token.Kind.VAR -> NULL,
+ Token.Kind.TYPE_IDENT -> NULL,
+ Token.Kind.TYPE_VAR -> NULL,
+ Token.Kind.NAT -> NULL,
+ Token.Kind.FLOAT -> NULL,
+ Token.Kind.STRING -> LITERAL1,
+ Token.Kind.ALT_STRING -> LITERAL2,
+ Token.Kind.VERBATIM -> COMMENT3,
+ Token.Kind.SPACE -> NULL,
+ Token.Kind.COMMENT -> COMMENT1,
+ Token.Kind.UNPARSED -> INVALID
+ ).withDefaultValue(NULL)
+ }
+
+ def token_markup(syntax: Outer_Syntax, token: Token): Byte =
+ if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
+ else if (token.is_operator) JEditToken.OPERATOR
+ else token_style(token.kind)
+}
--- a/src/Tools/jEdit/src/session_dockable.scala Mon Nov 28 20:31:53 2011 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Mon Nov 28 20:39:08 2011 +0100
@@ -114,9 +114,9 @@
var end = size.width - insets.right
for {
(n, color) <- List(
- (st.unprocessed, Isabelle_Markup.unprocessed1_color),
- (st.running, Isabelle_Markup.running_color),
- (st.failed, Isabelle_Markup.error_color)) }
+ (st.unprocessed, Isabelle_Rendering.unprocessed1_color),
+ (st.running, Isabelle_Rendering.running_color),
+ (st.failed, Isabelle_Rendering.error_color)) }
{
gfx.setColor(color)
val v = (n * w / st.total) max (if (n > 0) 2 else 0)
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Nov 28 20:31:53 2011 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Nov 28 20:39:08 2011 +0100
@@ -95,7 +95,7 @@
if !command.is_ignored
range <- line_range.try_restrict(snapshot.convert(command.range + command_start))
r <- Isabelle.gfx_range(text_area, range)
- color <- Isabelle_Markup.status_color(snapshot, command)
+ color <- Isabelle_Rendering.status_color(snapshot, command)
} {
gfx.setColor(color)
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
@@ -104,7 +104,7 @@
// background color (1): markup
for {
Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
+ snapshot.select_markup(line_range)(Isabelle_Rendering.background1).iterator
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -114,7 +114,7 @@
// background color (2): markup
for {
Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
+ snapshot.select_markup(line_range)(Isabelle_Rendering.background2).iterator
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -124,7 +124,7 @@
// squiggly underline
for {
Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
+ snapshot.select_markup(line_range)(Isabelle_Rendering.message).iterator
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -215,7 +215,7 @@
val markup =
for {
- r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color)
+ r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Rendering.text_color)
r2 <- r1.try_restrict(chunk_range)
} yield r2
@@ -317,7 +317,7 @@
// foreground color
for {
Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.foreground).iterator
+ snapshot.select_markup(line_range)(Isabelle_Rendering.foreground).iterator
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
--- a/src/Tools/jEdit/src/token_markup.scala Mon Nov 28 20:31:53 2011 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Nov 28 20:39:08 2011 +0100
@@ -178,7 +178,7 @@
if (line_ctxt.isDefined && Isabelle.session.is_ready) {
val syntax = Isabelle.session.current_syntax()
val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
- val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok))
+ val styled_tokens = tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
(styled_tokens, new Line_Context(Some(ctxt1)))
}
else {