wenzelm@43282: /*  Title:      Tools/jEdit/src/isabelle_markup.scala
wenzelm@39178:     Author:     Makarius
wenzelm@39178: 
wenzelm@39178: Isabelle specific physical rendering and markup selection.
wenzelm@39178: */
wenzelm@39178: 
wenzelm@39178: package isabelle.jedit
wenzelm@39178: 
wenzelm@39178: 
wenzelm@39178: import isabelle._
wenzelm@39178: 
wenzelm@39178: import java.awt.Color
wenzelm@39178: 
wenzelm@43386: import org.lobobrowser.util.gui.ColorFactory
wenzelm@43414: import org.gjt.sp.jedit.syntax.{Token => JEditToken}
wenzelm@39178: 
wenzelm@39178: 
wenzelm@39178: object Isabelle_Markup
wenzelm@39178: {
wenzelm@39178:   /* physical rendering */
wenzelm@39178: 
wenzelm@43377:   // see http://www.w3schools.com/css/css_colornames.asp
wenzelm@43377: 
wenzelm@43386:   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
wenzelm@43386: 
wenzelm@39178:   val outdated_color = new Color(240, 240, 240)
wenzelm@39178:   val unfinished_color = new Color(255, 228, 225)
wenzelm@39178: 
wenzelm@39690:   val light_color = new Color(240, 240, 240)
wenzelm@39178:   val regular_color = new Color(192, 192, 192)
wenzelm@39692:   val warning_color = new Color(255, 140, 0)
wenzelm@39691:   val error_color = new Color(178, 34, 34)
wenzelm@39690:   val bad_color = new Color(255, 106, 106, 100)
wenzelm@42171:   val hilite_color = new Color(255, 204, 102, 100)
wenzelm@39178: 
wenzelm@43435:   val subexp_color = new Color(0xC0, 0xC0, 0xC0, 100)
wenzelm@43435: 
wenzelm@43388:   val keyword1_color = get_color("#006699")
wenzelm@43388:   val keyword2_color = get_color("#009966")
wenzelm@43388: 
wenzelm@39181:   class Icon(val priority: Int, val icon: javax.swing.Icon)
wenzelm@39181:   {
wenzelm@39181:     def >= (that: Icon): Boolean = this.priority >= that.priority
wenzelm@39181:   }
wenzelm@39241:   val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
wenzelm@39241:   val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
wenzelm@39178: 
wenzelm@39178: 
wenzelm@39178:   /* command status */
wenzelm@39178: 
wenzelm@39178:   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178:   {
wenzelm@39178:     val state = snapshot.state(command)
wenzelm@39178:     if (snapshot.is_outdated) Some(outdated_color)
wenzelm@39178:     else
wenzelm@39178:       Isar_Document.command_status(state.status) match {
wenzelm@39178:         case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39178:         case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178:         case _ => None
wenzelm@39178:       }
wenzelm@39178:   }
wenzelm@39178: 
wenzelm@39178:   def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178:   {
wenzelm@39178:     val state = snapshot.state(command)
wenzelm@39178:     if (snapshot.is_outdated) None
wenzelm@39178:     else
wenzelm@39178:       Isar_Document.command_status(state.status) match {
wenzelm@39512:         case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
wenzelm@39178:         case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178:         case Isar_Document.Failed => Some(error_color)
wenzelm@39512:         case Isar_Document.Finished =>
wenzelm@39512:           if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
wenzelm@39512:           else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
wenzelm@39512:           else None
wenzelm@39178:       }
wenzelm@39178:   }
wenzelm@39178: 
wenzelm@39178: 
wenzelm@39178:   /* markup selectors */
wenzelm@39178: 
wenzelm@39178:   val message: Markup_Tree.Select[Color] =
wenzelm@39178:   {
wenzelm@39178:     case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
wenzelm@39178:     case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
wenzelm@39178:     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
wenzelm@39178:   }
wenzelm@39178: 
wenzelm@40338:   val popup: Markup_Tree.Select[String] =
wenzelm@39740:   {
wenzelm@39740:     case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
wenzelm@40338:     if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
wenzelm@40339:       Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@39740:   }
wenzelm@39740: 
wenzelm@39181:   val gutter_message: Markup_Tree.Select[Icon] =
wenzelm@39181:   {
wenzelm@39181:     case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
wenzelm@39181:     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
wenzelm@39181:   }
wenzelm@39181: 
wenzelm@39700:   val background1: Markup_Tree.Select[Color] =
wenzelm@39178:   {
wenzelm@39178:     case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
wenzelm@42171:     case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
wenzelm@39178:   }
wenzelm@39178: 
wenzelm@39700:   val background2: Markup_Tree.Select[Color] =
wenzelm@39178:   {
wenzelm@39690:     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
wenzelm@39178:   }
wenzelm@39178: 
wenzelm@43548:   private val text_entity_colors: Map[String, Color] =
wenzelm@43548:     Map(
wenzelm@43552:       Markup.CLASS -> get_color("red"),
wenzelm@43552:       Markup.TYPE -> get_color("black"),
wenzelm@43589:       Markup.CONSTANT -> get_color("black"))
wenzelm@43548: 
wenzelm@43434:   private val text_colors: Map[String, Color] =
wenzelm@43386:     Map(
wenzelm@43436:       Markup.LITERAL -> keyword1_color,
wenzelm@43436:       Markup.DELIMITER -> get_color("black"),
wenzelm@43436:       Markup.IDENT -> get_color("black"),
wenzelm@43386:       Markup.TFREE -> get_color("#A020F0"),
wenzelm@43386:       Markup.TVAR -> get_color("#A020F0"),
wenzelm@43386:       Markup.FREE -> get_color("blue"),
wenzelm@43386:       Markup.SKOLEM -> get_color("#D2691E"),
wenzelm@43386:       Markup.BOUND -> get_color("green"),
wenzelm@43386:       Markup.VAR -> get_color("#00009B"),
wenzelm@43386:       Markup.INNER_STRING -> get_color("#D2691E"),
wenzelm@43386:       Markup.INNER_COMMENT -> get_color("#8B0000"),
wenzelm@43386:       Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
wenzelm@43388:       Markup.ML_KEYWORD -> keyword1_color,
wenzelm@43386:       Markup.ML_DELIMITER -> get_color("black"),
wenzelm@43386:       Markup.ML_NUMERAL -> get_color("red"),
wenzelm@43386:       Markup.ML_CHAR -> get_color("#D2691E"),
wenzelm@43386:       Markup.ML_STRING -> get_color("#D2691E"),
wenzelm@43386:       Markup.ML_COMMENT -> get_color("#8B0000"),
wenzelm@43431:       Markup.ML_MALFORMED -> get_color("#FF6A6A"),
wenzelm@43431:       Markup.ANTIQ -> get_color("blue"))
wenzelm@43386: 
wenzelm@43434:   val text_color: Markup_Tree.Select[Color] =
wenzelm@43376:   {
wenzelm@43548:     case Text.Info(_, XML.Elem(Markup.Entity(kind, _), _))
wenzelm@43548:     if text_entity_colors.isDefinedAt(kind) => text_entity_colors(kind)
wenzelm@43386:     case Text.Info(_, XML.Elem(Markup(m, _), _))
wenzelm@43434:     if text_colors.isDefinedAt(m) => text_colors(m)
wenzelm@43376:   }
wenzelm@43376: 
wenzelm@43431:   private val tooltips: Map[String, String] =
wenzelm@43431:     Map(
wenzelm@43431:       Markup.SORT -> "sort",
wenzelm@43431:       Markup.TYP -> "type",
wenzelm@43431:       Markup.TERM -> "term",
wenzelm@43431:       Markup.PROP -> "proposition",
wenzelm@43431:       Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@43431:       Markup.FREE -> "free variable (globally fixed)",
wenzelm@43431:       Markup.SKOLEM -> "skolem variable (locally fixed)",
wenzelm@43431:       Markup.BOUND -> "bound variable (internally fixed)",
wenzelm@43431:       Markup.VAR -> "schematic variable",
wenzelm@43431:       Markup.TFREE -> "free type variable",
wenzelm@43431:       Markup.TVAR -> "schematic type variable",
wenzelm@43431:       Markup.ML_SOURCE -> "ML source",
wenzelm@43431:       Markup.DOC_SOURCE -> "document source")
wenzelm@43431: 
wenzelm@39178:   val tooltip: Markup_Tree.Select[String] =
wenzelm@39178:   {
wenzelm@44181:     case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
wenzelm@39178:     case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@40339:       Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
wenzelm@40339:         margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@43431:     case Text.Info(_, XML.Elem(Markup(name, _), _))
wenzelm@43431:     if tooltips.isDefinedAt(name) => tooltips(name)
wenzelm@42302:   }
wenzelm@42302: 
wenzelm@42302:   private val subexp_include =
wenzelm@42302:     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
wenzelm@42302:       Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
wenzelm@43431:       Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
wenzelm@42302: 
wenzelm@42302:   val subexp: Markup_Tree.Select[(Text.Range, Color)] =
wenzelm@42302:   {
wenzelm@42302:     case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@43435:       (range, subexp_color)
wenzelm@39178:   }
wenzelm@39179: 
wenzelm@39179: 
wenzelm@39179:   /* token markup -- text styles */
wenzelm@39179: 
wenzelm@39179:   private val command_style: Map[String, Byte] =
wenzelm@39179:   {
wenzelm@43414:     import JEditToken._
wenzelm@39179:     Map[String, Byte](
wenzelm@39179:       Keyword.THY_END -> KEYWORD2,
wenzelm@39179:       Keyword.THY_SCRIPT -> LABEL,
wenzelm@39179:       Keyword.PRF_SCRIPT -> LABEL,
wenzelm@39179:       Keyword.PRF_ASM -> KEYWORD3,
wenzelm@39179:       Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@39179:     ).withDefaultValue(KEYWORD1)
wenzelm@39179:   }
wenzelm@39179: 
wenzelm@43414:   private val token_style: Map[Token.Kind.Value, Byte] =
wenzelm@39179:   {
wenzelm@43414:     import JEditToken._
wenzelm@43414:     Map[Token.Kind.Value, Byte](
wenzelm@43414:       Token.Kind.KEYWORD -> KEYWORD2,
wenzelm@43414:       Token.Kind.IDENT -> NULL,
wenzelm@43414:       Token.Kind.LONG_IDENT -> NULL,
wenzelm@43414:       Token.Kind.SYM_IDENT -> NULL,
wenzelm@43414:       Token.Kind.VAR -> NULL,
wenzelm@43414:       Token.Kind.TYPE_IDENT -> NULL,
wenzelm@43414:       Token.Kind.TYPE_VAR -> NULL,
wenzelm@43414:       Token.Kind.NAT -> NULL,
wenzelm@43414:       Token.Kind.FLOAT -> NULL,
wenzelm@43431:       Token.Kind.STRING -> LITERAL1,
wenzelm@43431:       Token.Kind.ALT_STRING -> LITERAL2,
wenzelm@43414:       Token.Kind.VERBATIM -> COMMENT3,
wenzelm@43414:       Token.Kind.SPACE -> NULL,
wenzelm@43414:       Token.Kind.COMMENT -> COMMENT1,
wenzelm@43414:       Token.Kind.UNPARSED -> INVALID
wenzelm@39179:     ).withDefaultValue(NULL)
wenzelm@39179:   }
wenzelm@39179: 
wenzelm@43414:   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
wenzelm@43430:     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
wenzelm@43430:     else if (token.is_operator) JEditToken.OPERATOR
wenzelm@43414:     else token_style(token.kind)
wenzelm@39178: }