src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Wed Sep 12 13:21:33 2012 +0200 (2012-09-12 ago)
changeset 49321 a48f9bbbe720
parent 49294 a600c017f814
child 49355 7d1af0a6e797
permissions -rw-r--r--
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
     1 /*  Title:      Tools/jEdit/src/isabelle_rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle specific physical rendering and markup selection.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.Color
    13 import javax.swing.Icon
    14 import java.io.{File => JFile}
    15 
    16 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    17 
    18 import scala.collection.immutable.SortedMap
    19 
    20 
    21 object Isabelle_Rendering
    22 {
    23   /* physical rendering */
    24 
    25   def color_value(s: String): Color = Color_Value(Isabelle.options.value.string(s))
    26 
    27   private val writeln_pri = 1
    28   private val warning_pri = 2
    29   private val legacy_pri = 3
    30   private val error_pri = 4
    31 
    32 
    33   /* command overview */
    34 
    35   def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
    36   {
    37     if (snapshot.is_outdated) None
    38     else {
    39       val results =
    40         snapshot.cumulate_markup[(Protocol.Status, Int)](
    41           range, (Protocol.Status.init, 0),
    42           Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
    43           {
    44             case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
    45               if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
    46               else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
    47               else (Protocol.command_status(status, markup), pri)
    48           })
    49       if (results.isEmpty) None
    50       else {
    51         val (status, pri) =
    52           ((Protocol.Status.init, 0) /: results) {
    53             case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
    54 
    55         if (pri == warning_pri) Some(color_value("color_warning"))
    56         else if (pri == error_pri) Some(color_value("color_error"))
    57         else if (status.is_unprocessed) Some(color_value("color_unprocessed"))
    58         else if (status.is_running) Some(color_value("color_running"))
    59         else if (status.is_failed) Some(color_value("color_error"))
    60         else None
    61       }
    62     }
    63   }
    64 
    65 
    66   /* markup selectors */
    67 
    68   private val subexp_include =
    69     Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
    70       Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
    71       Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
    72       Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
    73       Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
    74 
    75   def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
    76   {
    77     snapshot.select_markup(range, Some(subexp_include),
    78         {
    79           case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
    80             Text.Info(snapshot.convert(info_range), color_value("color_subexp"))
    81         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    82   }
    83 
    84 
    85   private val hyperlink_include = Set(Isabelle_Markup.ENTITY, Isabelle_Markup.PATH)
    86 
    87   def hyperlink(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Hyperlink]] =
    88   {
    89     snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
    90         {
    91           case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
    92           if Path.is_ok(name) =>
    93             val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    94             Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
    95 
    96           case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
    97           if (props.find(
    98             { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
    99               case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
   100               case _ => false }).isEmpty) =>
   101 
   102             props match {
   103               case Position.Line_File(line, name) if Path.is_ok(name) =>
   104                 Isabelle_System.source_file(Path.explode(name)) match {
   105                   case Some(path) =>
   106                     val jedit_file = Isabelle_System.platform_path(path)
   107                     Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
   108                   case None => links
   109                 }
   110 
   111               case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
   112                 snapshot.state.find_command(snapshot.version, id) match {
   113                   case Some((node, command)) =>
   114                     val sources =
   115                       node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   116                         Iterator.single(command.source(Text.Range(0, command.decode(offset))))
   117                     val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   118                     Text.Info(snapshot.convert(info_range),
   119                       Hyperlink(command.node_name.node, line, column)) :: links
   120                   case None => links
   121                 }
   122 
   123               case _ => links
   124             }
   125         }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
   126   }
   127 
   128 
   129   private def tooltip_text(msg: XML.Tree): String =
   130     Pretty.string_of(List(msg), margin = Isabelle.options.int("jedit_tooltip_margin"))
   131 
   132   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   133   {
   134     val msgs =
   135       snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
   136         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
   137           Isabelle_Markup.BAD)),
   138         {
   139           case (msgs, Text.Info(_, msg @
   140               XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
   141           if markup == Isabelle_Markup.WRITELN ||
   142               markup == Isabelle_Markup.WARNING ||
   143               markup == Isabelle_Markup.ERROR =>
   144             msgs + (serial -> tooltip_text(msg))
   145           case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
   146           if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg))
   147         }).toList.flatMap(_.info)
   148     if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
   149   }
   150 
   151 
   152   private val tooltips: Map[String, String] =
   153     Map(
   154       Isabelle_Markup.SORT -> "sort",
   155       Isabelle_Markup.TYP -> "type",
   156       Isabelle_Markup.TERM -> "term",
   157       Isabelle_Markup.PROP -> "proposition",
   158       Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
   159       Isabelle_Markup.FREE -> "free variable",
   160       Isabelle_Markup.SKOLEM -> "skolem variable",
   161       Isabelle_Markup.BOUND -> "bound variable",
   162       Isabelle_Markup.VAR -> "schematic variable",
   163       Isabelle_Markup.TFREE -> "free type variable",
   164       Isabelle_Markup.TVAR -> "schematic type variable",
   165       Isabelle_Markup.ML_SOURCE -> "ML source",
   166       Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
   167 
   168   private val tooltip_elements =
   169     Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
   170       Isabelle_Markup.PATH) ++ tooltips.keys
   171 
   172   private def string_of_typing(kind: String, body: XML.Body): String =
   173     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
   174       margin = Isabelle.options.int("jedit_tooltip_margin"))
   175 
   176   def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   177   {
   178     def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) =
   179       if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
   180 
   181     val tips =
   182       snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]](
   183         range, Text.Info(range, Nil), Some(tooltip_elements),
   184         {
   185           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
   186             val kind1 = space_explode('_', kind).mkString(" ")
   187             add(prev, r, (true, kind1 + " " + quote(name)))
   188           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
   189           if Path.is_ok(name) =>
   190             val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   191             add(prev, r, (true, "file " + quote(jedit_file)))
   192           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
   193             add(prev, r, (true, string_of_typing("::", body)))
   194           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
   195             add(prev, r, (false, string_of_typing("ML:", body)))
   196           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   197           if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))
   198         }).toList.flatMap(_.info.info)
   199 
   200     val all_tips =
   201       (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   202     if (all_tips.isEmpty) None else Some(cat_lines(all_tips))
   203   }
   204 
   205 
   206   private val gutter_icons = Map(
   207     warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
   208     legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
   209     error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
   210 
   211   def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
   212   {
   213     val results =
   214       snapshot.cumulate_markup[Int](range, 0,
   215         Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   216         {
   217           case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
   218             body match {
   219               case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
   220               case _ => pri max warning_pri
   221             }
   222           case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
   223             pri max error_pri
   224         })
   225     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   226     gutter_icons.get(pri)
   227   }
   228 
   229 
   230   def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   231   {
   232     val squiggly_colors = Map(
   233       writeln_pri -> color_value("color_writeln"),
   234       warning_pri -> color_value("color_warning"),
   235       error_pri -> color_value("color_error"))
   236 
   237     val results =
   238       snapshot.cumulate_markup[Int](range, 0,
   239         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   240         {
   241           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
   242             name match {
   243               case Isabelle_Markup.WRITELN => pri max writeln_pri
   244               case Isabelle_Markup.WARNING => pri max warning_pri
   245               case Isabelle_Markup.ERROR => pri max error_pri
   246               case _ => pri
   247             }
   248         })
   249     for {
   250       Text.Info(r, pri) <- results
   251       color <- squiggly_colors.get(pri)
   252     } yield Text.Info(r, color)
   253   }
   254 
   255 
   256   def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   257   {
   258     if (snapshot.is_outdated) Stream(Text.Info(range, color_value("color_outdated")))
   259     else
   260       for {
   261         Text.Info(r, result) <-
   262           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   263             range, (Some(Protocol.Status.init), None),
   264             Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
   265             {
   266               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   267               if (Protocol.command_status_markup(markup.name)) =>
   268                 (Some(Protocol.command_status(status, markup)), color)
   269               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
   270                 (None, Some(color_value("color_bad")))
   271               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
   272                 (None, Some(color_value("color_hilite")))
   273             })
   274         color <-
   275           (result match {
   276             case (Some(status), opt_color) =>
   277               if (status.is_unprocessed) Some(color_value("color_unprocessed1"))
   278               else if (status.is_running) Some(color_value("color_running1"))
   279               else opt_color
   280             case (_, opt_color) => opt_color
   281           })
   282       } yield Text.Info(r, color)
   283   }
   284 
   285 
   286   def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   287     snapshot.select_markup(range,
   288       Some(Set(Isabelle_Markup.TOKEN_RANGE)),
   289       {
   290         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) =>
   291           color_value("color_light")
   292       })
   293 
   294 
   295   def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   296     snapshot.select_markup(range,
   297       Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
   298       {
   299         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) =>
   300           color_value("color_quoted")
   301         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) =>
   302           color_value("color_quoted")
   303         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) =>
   304           color_value("color_quoted")
   305       })
   306 
   307 
   308   def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
   309       : Stream[Text.Info[Color]] =
   310   {
   311     val text_colors: Map[String, Color] = Map(
   312       Isabelle_Markup.STRING -> Color.BLACK,
   313       Isabelle_Markup.ALTSTRING -> Color.BLACK,
   314       Isabelle_Markup.VERBATIM -> Color.BLACK,
   315       Isabelle_Markup.LITERAL -> color_value("color_keyword1"),
   316       Isabelle_Markup.DELIMITER -> Color.BLACK,
   317       Isabelle_Markup.TFREE -> color_value("color_variable_type"),
   318       Isabelle_Markup.TVAR -> color_value("color_variable_type"),
   319       Isabelle_Markup.FREE -> color_value("color_variable_free"),
   320       Isabelle_Markup.SKOLEM -> color_value("color_variable_skolem"),
   321       Isabelle_Markup.BOUND -> color_value("color_variable_bound"),
   322       Isabelle_Markup.VAR -> color_value("color_variable_schematic"),
   323       Isabelle_Markup.INNER_STRING -> color_value("color_inner_quoted"),
   324       Isabelle_Markup.INNER_COMMENT -> color_value("color_inner_comment"),
   325       Isabelle_Markup.DYNAMIC_FACT -> color_value("color_dynamic"),
   326       Isabelle_Markup.ML_KEYWORD -> color_value("color_keyword1"),
   327       Isabelle_Markup.ML_DELIMITER -> Color.BLACK,
   328       Isabelle_Markup.ML_NUMERAL -> color_value("color_inner_numeral"),
   329       Isabelle_Markup.ML_CHAR -> color_value("color_inner_quoted"),
   330       Isabelle_Markup.ML_STRING -> color_value("color_inner_quoted"),
   331       Isabelle_Markup.ML_COMMENT -> color_value("color_inner_comment"),
   332       Isabelle_Markup.ANTIQ -> color_value("color_antiquotation"))
   333 
   334     val text_color_elements = Set.empty[String] ++ text_colors.keys
   335 
   336     snapshot.cumulate_markup(range, color, Some(text_color_elements),
   337       {
   338         case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   339         if text_colors.isDefinedAt(m) => text_colors(m)
   340       })
   341   }
   342 
   343 
   344   /* token markup -- text styles */
   345 
   346   private val command_style: Map[String, Byte] =
   347   {
   348     import JEditToken._
   349     Map[String, Byte](
   350       Keyword.THY_END -> KEYWORD2,
   351       Keyword.THY_SCRIPT -> LABEL,
   352       Keyword.PRF_SCRIPT -> LABEL,
   353       Keyword.PRF_ASM -> KEYWORD3,
   354       Keyword.PRF_ASM_GOAL -> KEYWORD3
   355     ).withDefaultValue(KEYWORD1)
   356   }
   357 
   358   private val token_style: Map[Token.Kind.Value, Byte] =
   359   {
   360     import JEditToken._
   361     Map[Token.Kind.Value, Byte](
   362       Token.Kind.KEYWORD -> KEYWORD2,
   363       Token.Kind.IDENT -> NULL,
   364       Token.Kind.LONG_IDENT -> NULL,
   365       Token.Kind.SYM_IDENT -> NULL,
   366       Token.Kind.VAR -> NULL,
   367       Token.Kind.TYPE_IDENT -> NULL,
   368       Token.Kind.TYPE_VAR -> NULL,
   369       Token.Kind.NAT -> NULL,
   370       Token.Kind.FLOAT -> NULL,
   371       Token.Kind.STRING -> LITERAL1,
   372       Token.Kind.ALT_STRING -> LITERAL2,
   373       Token.Kind.VERBATIM -> COMMENT3,
   374       Token.Kind.SPACE -> NULL,
   375       Token.Kind.COMMENT -> COMMENT1,
   376       Token.Kind.ERROR -> INVALID
   377     ).withDefaultValue(NULL)
   378   }
   379 
   380   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
   381     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
   382     else if (token.is_operator) JEditToken.OPERATOR
   383     else token_style(token.kind)
   384 }