# HG changeset patch # User wenzelm # Date 1326716384 -3600 # Node ID de441d4ff1be3f9c8425071d5ca9b2255b3f2b90 # Parent f23dc7d16c0b7667e9d1a1d0214d321a3c8d3d26 tuned; diff -r f23dc7d16c0b -r de441d4ff1be src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Mon Jan 16 07:55:10 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Mon Jan 16 13:19:44 2012 +0100 @@ -87,6 +87,23 @@ /* markup selectors */ + private val subexp_include = + Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP, + Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY, + Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, + Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, + Isabelle_Markup.DOC_SOURCE) + + def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] = + { + snapshot.select_markup(range, Some(subexp_include), + { + case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => + Text.Info(snapshot.convert(range), subexp_color) + }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None } + } + + def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] = { val msgs = @@ -103,133 +120,6 @@ if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2))) } - private val gutter_icons = Map( - warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"), - legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"), - error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png")) - - def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] = - { - val results = - snapshot.cumulate_markup[Int](range, 0, - Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), - { - case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) => - body match { - case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri - case _ => pri max warning_pri - } - case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) => - pri max error_pri - }) - val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 } - gutter_icons.get(pri) - } - - private val squiggly_colors = Map( - writeln_pri -> writeln_color, - warning_pri -> warning_color, - error_pri -> error_color) - - def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = - { - val results = - snapshot.cumulate_markup[Int](range, 0, - Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), - { - case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) => - name match { - case Isabelle_Markup.WRITELN => pri max writeln_pri - case Isabelle_Markup.WARNING => pri max warning_pri - case Isabelle_Markup.ERROR => pri max error_pri - case _ => pri - } - }) - for { - Text.Info(r, pri) <- results - color <- squiggly_colors.get(pri) - } yield Text.Info(r, color) - } - - def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = - { - if (snapshot.is_outdated) Stream(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), - Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE), - { - case (((Some(status), color), Text.Info(_, XML.Elem(markup, _)))) - if (Protocol.command_status_markup(markup.name)) => - (Some(Protocol.command_status(status, markup)), color) - case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) => - (None, Some(bad_color)) - case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) => - (None, Some(hilite_color)) - }) - color <- - (result match { - case (Some(status), _) => - if (status.is_running) Some(running1_color) - else if (status.is_unprocessed) Some(unprocessed1_color) - else None - case (_, opt_color) => opt_color - }) - } yield Text.Info(r, color) - } - - def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = - snapshot.select_markup(range, - Some(Set(Isabelle_Markup.TOKEN_RANGE)), - { - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color - }) - - def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = - snapshot.select_markup(range, - Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)), - { - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color - case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color - }) - - private val text_colors: Map[String, Color] = - Map( - Isabelle_Markup.STRING -> get_color("black"), - Isabelle_Markup.ALTSTRING -> get_color("black"), - Isabelle_Markup.VERBATIM -> get_color("black"), - Isabelle_Markup.LITERAL -> keyword1_color, - Isabelle_Markup.DELIMITER -> get_color("black"), - Isabelle_Markup.TFREE -> get_color("#A020F0"), - Isabelle_Markup.TVAR -> get_color("#A020F0"), - Isabelle_Markup.FREE -> get_color("blue"), - Isabelle_Markup.SKOLEM -> get_color("#D2691E"), - Isabelle_Markup.BOUND -> get_color("green"), - Isabelle_Markup.VAR -> get_color("#00009B"), - Isabelle_Markup.INNER_STRING -> get_color("#D2691E"), - Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"), - Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"), - Isabelle_Markup.ML_KEYWORD -> keyword1_color, - Isabelle_Markup.ML_DELIMITER -> get_color("black"), - Isabelle_Markup.ML_NUMERAL -> get_color("red"), - Isabelle_Markup.ML_CHAR -> get_color("#D2691E"), - Isabelle_Markup.ML_STRING -> get_color("#D2691E"), - Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"), - Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"), - Isabelle_Markup.ANTIQ -> get_color("blue")) - - private val text_color_elements = Set.empty[String] ++ text_colors.keys - - def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color) - : Stream[Text.Info[Color]] = - snapshot.cumulate_markup(range, color, Some(text_color_elements), - { - case (_, Text.Info(_, XML.Elem(Markup(m, _), _))) - if text_colors.isDefinedAt(m) => text_colors(m) - }) private val tooltips: Map[String, String] = Map( @@ -278,23 +168,141 @@ if (tips.isEmpty) None else Some(cat_lines(tips)) } - private val subexp_include = - Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP, - Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY, - Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND, - Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE, - Isabelle_Markup.DOC_SOURCE) + + private val gutter_icons = Map( + warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"), + legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"), + error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png")) + + def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] = + { + val results = + snapshot.cumulate_markup[Int](range, 0, + Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), + { + case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) => + body match { + case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri + case _ => pri max warning_pri + } + case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) => + pri max error_pri + }) + val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 } + gutter_icons.get(pri) + } + + + private val squiggly_colors = Map( + writeln_pri -> writeln_color, + warning_pri -> warning_color, + error_pri -> error_color) + + def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = + { + val results = + snapshot.cumulate_markup[Int](range, 0, + Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)), + { + case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) => + name match { + case Isabelle_Markup.WRITELN => pri max writeln_pri + case Isabelle_Markup.WARNING => pri max warning_pri + case Isabelle_Markup.ERROR => pri max error_pri + case _ => pri + } + }) + for { + Text.Info(r, pri) <- results + color <- squiggly_colors.get(pri) + } yield Text.Info(r, color) + } + - def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] = + def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = { - snapshot.select_markup(range, Some(subexp_include), - { - case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => - Text.Info(snapshot.convert(range), subexp_color) - }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None } + if (snapshot.is_outdated) Stream(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), + Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE), + { + case (((Some(status), color), Text.Info(_, XML.Elem(markup, _)))) + if (Protocol.command_status_markup(markup.name)) => + (Some(Protocol.command_status(status, markup)), color) + case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) => + (None, Some(bad_color)) + case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) => + (None, Some(hilite_color)) + }) + color <- + (result match { + case (Some(status), _) => + if (status.is_running) Some(running1_color) + else if (status.is_unprocessed) Some(unprocessed1_color) + else None + case (_, opt_color) => opt_color + }) + } yield Text.Info(r, color) } + def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = + snapshot.select_markup(range, + Some(Set(Isabelle_Markup.TOKEN_RANGE)), + { + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color + }) + + + def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] = + snapshot.select_markup(range, + Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)), + { + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color + case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color + }) + + + private val text_colors: Map[String, Color] = + Map( + Isabelle_Markup.STRING -> get_color("black"), + Isabelle_Markup.ALTSTRING -> get_color("black"), + Isabelle_Markup.VERBATIM -> get_color("black"), + Isabelle_Markup.LITERAL -> keyword1_color, + Isabelle_Markup.DELIMITER -> get_color("black"), + Isabelle_Markup.TFREE -> get_color("#A020F0"), + Isabelle_Markup.TVAR -> get_color("#A020F0"), + Isabelle_Markup.FREE -> get_color("blue"), + Isabelle_Markup.SKOLEM -> get_color("#D2691E"), + Isabelle_Markup.BOUND -> get_color("green"), + Isabelle_Markup.VAR -> get_color("#00009B"), + Isabelle_Markup.INNER_STRING -> get_color("#D2691E"), + Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"), + Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"), + Isabelle_Markup.ML_KEYWORD -> keyword1_color, + Isabelle_Markup.ML_DELIMITER -> get_color("black"), + Isabelle_Markup.ML_NUMERAL -> get_color("red"), + Isabelle_Markup.ML_CHAR -> get_color("#D2691E"), + Isabelle_Markup.ML_STRING -> get_color("#D2691E"), + Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"), + Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"), + Isabelle_Markup.ANTIQ -> get_color("blue")) + + private val text_color_elements = Set.empty[String] ++ text_colors.keys + + def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color) + : Stream[Text.Info[Color]] = + snapshot.cumulate_markup(range, color, Some(text_color_elements), + { + case (_, Text.Info(_, XML.Elem(Markup(m, _), _))) + if text_colors.isDefinedAt(m) => text_colors(m) + }) + + /* token markup -- text styles */ private val command_style: Map[String, Byte] =