# HG changeset patch # User wenzelm # Date 1322509148 -3600 # Node ID 129db14167170137961c8f6be31b9cb40bcf66da # Parent ac6e704dcd12fa618dd1bc2efd520a9d2dce1a22 renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module; diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/src/document_view.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) diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/src/isabelle_markup.scala --- 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) -} diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/src/isabelle_rendering.scala --- /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) +} diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/src/session_dockable.scala --- 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) diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/src/text_area_painter.scala --- 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) diff -r ac6e704dcd12 -r 129db1416717 src/Tools/jEdit/src/token_markup.scala --- 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 {