merged
authorwenzelm
Wed Sep 08 14:46:21 2010 +0200 (2010-09-08)
changeset 392187f4fb691e4b6
parent 39217 1d5e81f5f083
parent 39182 cce0c10ed943
child 39223 022f16801e4e
merged
     1.1 --- a/src/Pure/General/markup.ML	Wed Sep 08 13:30:41 2010 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Wed Sep 08 14:46:21 2010 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4    val literalN: string val literal: T
     1.5    val inner_stringN: string val inner_string: T
     1.6    val inner_commentN: string val inner_comment: T
     1.7 +  val token_rangeN: string val token_range: T
     1.8    val sortN: string val sort: T
     1.9    val typN: string val typ: T
    1.10    val termN: string val term: T
    1.11 @@ -119,6 +120,7 @@
    1.12    val promptN: string val prompt: T
    1.13    val readyN: string val ready: T
    1.14    val reportN: string val report: T
    1.15 +  val badN: string val bad: T
    1.16    val no_output: output * output
    1.17    val default_output: T -> output * output
    1.18    val add_mode: string -> (T -> output * output) -> unit
    1.19 @@ -239,6 +241,8 @@
    1.20  val (inner_stringN, inner_string) = markup_elem "inner_string";
    1.21  val (inner_commentN, inner_comment) = markup_elem "inner_comment";
    1.22  
    1.23 +val (token_rangeN, token_range) = markup_elem "token_range";
    1.24 +
    1.25  val (sortN, sort) = markup_elem "sort";
    1.26  val (typN, typ) = markup_elem "typ";
    1.27  val (termN, term) = markup_elem "term";
    1.28 @@ -345,6 +349,8 @@
    1.29  
    1.30  val (reportN, report) = markup_elem "report";
    1.31  
    1.32 +val (badN, bad) = markup_elem "bad";
    1.33 +
    1.34  
    1.35  
    1.36  (** print mode operations **)
     2.1 --- a/src/Pure/General/markup.scala	Wed Sep 08 13:30:41 2010 +0100
     2.2 +++ b/src/Pure/General/markup.scala	Wed Sep 08 14:46:21 2010 +0200
     2.3 @@ -136,6 +136,8 @@
     2.4    val LITERAL = "literal"
     2.5    val INNER_COMMENT = "inner_comment"
     2.6  
     2.7 +  val TOKEN_RANGE = "token_range"
     2.8 +
     2.9    val SORT = "sort"
    2.10    val TYP = "typ"
    2.11    val TERM = "term"
    2.12 @@ -247,6 +249,8 @@
    2.13    val SIGNAL = "signal"
    2.14    val EXIT = "exit"
    2.15  
    2.16 +  val BAD = "bad"
    2.17 +
    2.18    val Ready = Markup("ready", Nil)
    2.19  
    2.20  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 08 13:30:41 2010 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Sep 08 14:46:21 2010 +0200
     3.3 @@ -736,18 +736,22 @@
     3.4  
     3.5  local
     3.6  
     3.7 +fun parse_failed ctxt pos msg kind =
     3.8 + (Context_Position.report ctxt Markup.bad pos;
     3.9 +  cat_error msg ("Failed to parse " ^ kind));
    3.10 +
    3.11  fun parse_sort ctxt text =
    3.12    let
    3.13      val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    3.14      val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
    3.15 -      handle ERROR msg => cat_error msg "Failed to parse sort";
    3.16 +      handle ERROR msg => parse_failed ctxt pos msg "sort";
    3.17    in Type.minimize_sort (tsig_of ctxt) S end;
    3.18  
    3.19  fun parse_typ ctxt text =
    3.20    let
    3.21      val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    3.22      val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
    3.23 -      handle ERROR msg => cat_error msg "Failed to parse type";
    3.24 +      handle ERROR msg => parse_failed ctxt pos msg "type";
    3.25    in T end;
    3.26  
    3.27  fun parse_term T ctxt text =
    3.28 @@ -764,7 +768,7 @@
    3.29      val t =
    3.30        Syntax.standard_parse_term check get_sort map_const map_free
    3.31          ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
    3.32 -      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
    3.33 +      handle ERROR msg => parse_failed ctxt pos msg kind;
    3.34    in t end;
    3.35  
    3.36  
     4.1 --- a/src/Pure/PIDE/command.scala	Wed Sep 08 13:30:41 2010 +0100
     4.2 +++ b/src/Pure/PIDE/command.scala	Wed Sep 08 14:46:21 2010 +0200
     4.3 @@ -48,11 +48,11 @@
     4.4          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
     4.5            (this /: msgs)((state, msg) =>
     4.6              msg match {
     4.7 -              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
     4.8 -              if id == command.id =>
     4.9 +              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
    4.10 +              if id == command.id && command.range.contains(command.decode(raw_range)) =>
    4.11 +                val range = command.decode(raw_range)
    4.12                  val props = Position.purge(atts)
    4.13 -                val info =
    4.14 -                  Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
    4.15 +                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
    4.16                  state.add_markup(info)
    4.17                case _ => System.err.println("Ignored report message: " + msg); state
    4.18              })
    4.19 @@ -60,8 +60,8 @@
    4.20            atts match {
    4.21              case Markup.Serial(i) =>
    4.22                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
    4.23 -              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
    4.24 -                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
    4.25 +              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
    4.26 +                (st, range) => st.add_markup(Text.Info(range, result)))
    4.27              case _ => System.err.println("Ignored message without serial number: " + message); this
    4.28            }
    4.29        }
     5.1 --- a/src/Pure/PIDE/document.scala	Wed Sep 08 13:30:41 2010 +0100
     5.2 +++ b/src/Pure/PIDE/document.scala	Wed Sep 08 14:46:21 2010 +0200
     5.3 @@ -169,11 +169,11 @@
     5.4      def lookup_command(id: Command_ID): Option[Command]
     5.5      def state(command: Command): Command.State
     5.6      def convert(i: Text.Offset): Text.Offset
     5.7 -    def convert(range: Text.Range): Text.Range = range.map(convert(_))
     5.8 +    def convert(range: Text.Range): Text.Range
     5.9      def revert(i: Text.Offset): Text.Offset
    5.10 -    def revert(range: Text.Range): Text.Range = range.map(revert(_))
    5.11 -    def select_markup[A](range: Text.Range)
    5.12 -      (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
    5.13 +    def revert(range: Text.Range): Text.Range
    5.14 +    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    5.15 +      : Stream[Text.Info[Option[A]]]
    5.16    }
    5.17  
    5.18    object State
    5.19 @@ -304,18 +304,24 @@
    5.20          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    5.21          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    5.22  
    5.23 -        def select_markup[A](range: Text.Range)
    5.24 -          (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
    5.25 +        def convert(range: Text.Range): Text.Range =
    5.26 +          if (edits.isEmpty) range else range.map(convert(_))
    5.27 +
    5.28 +        def revert(range: Text.Range): Text.Range =
    5.29 +          if (edits.isEmpty) range else range.map(revert(_))
    5.30 +
    5.31 +        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    5.32 +          : Stream[Text.Info[Option[A]]] =
    5.33          {
    5.34            val former_range = revert(range)
    5.35            for {
    5.36 -            (command, command_start) <- node.command_range(former_range)
    5.37 +            (command, command_start) <- node.command_range(former_range).toStream
    5.38              Text.Info(r0, x) <- state(command).markup.
    5.39                select((former_range - command_start).restrict(command.range)) {
    5.40                  case Text.Info(r0, info)
    5.41                  if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
    5.42                    result(Text.Info(convert(r0 + command_start), info))
    5.43 -              } { default }
    5.44 +              }
    5.45              val r = convert(r0 + command_start)
    5.46              if !r.is_singularity
    5.47            } yield Text.Info(r, x)
     6.1 --- a/src/Pure/PIDE/isar_document.scala	Wed Sep 08 13:30:41 2010 +0100
     6.2 +++ b/src/Pure/PIDE/isar_document.scala	Wed Sep 08 14:46:21 2010 +0200
     6.3 @@ -61,19 +61,27 @@
     6.4    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
     6.5    private val exclude_pos = Set(Markup.LOCATION)
     6.6  
     6.7 -  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
     6.8 +  private def is_state(msg: XML.Tree): Boolean =
     6.9 +    msg match {
    6.10 +      case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    6.11 +      case _ => false
    6.12 +    }
    6.13 +
    6.14 +  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    6.15    {
    6.16      def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    6.17        tree match {
    6.18 -        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    6.19 -        if include_pos(name) && id == command_id =>
    6.20 -          body.foldLeft(set + range)(reported)
    6.21 +        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    6.22 +        if include_pos(name) && id == command.id =>
    6.23 +          val range = command.decode(raw_range).restrict(command.range)
    6.24 +          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    6.25          case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    6.26            body.foldLeft(set)(reported)
    6.27          case _ => set
    6.28        }
    6.29      val set = reported(Set.empty, message)
    6.30 -    if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
    6.31 +    if (set.isEmpty && !is_state(message))
    6.32 +      set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    6.33      else set
    6.34    }
    6.35  }
     7.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Sep 08 13:30:41 2010 +0100
     7.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Sep 08 14:46:21 2010 +0200
     7.3 @@ -43,6 +43,8 @@
     7.4    }
     7.5  
     7.6    val empty = new Markup_Tree(Branches.empty)
     7.7 +
     7.8 +  type Select[A] = PartialFunction[Text.Info[Any], A]
     7.9  }
    7.10  
    7.11  
    7.12 @@ -89,11 +91,13 @@
    7.13    private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
    7.14      Branches.overlapping(range, branches).toStream
    7.15  
    7.16 -  def select[A](root_range: Text.Range)
    7.17 -    (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
    7.18 +  def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
    7.19 +    : Stream[Text.Info[Option[A]]] =
    7.20    {
    7.21 -    def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
    7.22 -      : Stream[Text.Info[A]] =
    7.23 +    def stream(
    7.24 +      last: Text.Offset,
    7.25 +      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
    7.26 +        : Stream[Text.Info[Option[A]]] =
    7.27      {
    7.28        stack match {
    7.29          case (parent, (range, (info, tree)) #:: more) :: rest =>
    7.30 @@ -102,7 +106,7 @@
    7.31            val start = subrange.start
    7.32  
    7.33            if (result.isDefinedAt(info)) {
    7.34 -            val next = Text.Info(subrange, result(info))
    7.35 +            val next = Text.Info[Option[A]](subrange, Some(result(info)))
    7.36              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
    7.37              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
    7.38              else nexts
    7.39 @@ -117,12 +121,11 @@
    7.40  
    7.41          case Nil =>
    7.42            val stop = root_range.stop
    7.43 -          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
    7.44 +          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
    7.45            else Stream.empty
    7.46        }
    7.47      }
    7.48 -    stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
    7.49 -      .iterator
    7.50 +    stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
    7.51    }
    7.52  
    7.53    def swing_tree(parent: DefaultMutableTreeNode)
     8.1 --- a/src/Pure/Syntax/lexicon.ML	Wed Sep 08 13:30:41 2010 +0100
     8.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Sep 08 14:46:21 2010 +0200
     8.3 @@ -66,6 +66,7 @@
     8.4    val terminals: string list
     8.5    val is_terminal: string -> bool
     8.6    val report_token: Proof.context -> token -> unit
     8.7 +  val report_token_range: Proof.context -> token -> unit
     8.8    val matching_tokens: token * token -> bool
     8.9    val valued_token: token -> bool
    8.10    val predef_term: string -> token option
    8.11 @@ -188,6 +189,11 @@
    8.12  fun report_token ctxt (Token (kind, _, (pos, _))) =
    8.13    Context_Position.report ctxt (token_kind_markup kind) pos;
    8.14  
    8.15 +fun report_token_range ctxt tok =
    8.16 +  if is_proper tok
    8.17 +  then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
    8.18 +  else ();
    8.19 +
    8.20  
    8.21  (* matching_tokens *)
    8.22  
     9.1 --- a/src/Pure/Syntax/syntax.ML	Wed Sep 08 13:30:41 2010 +0100
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Sep 08 14:46:21 2010 +0200
     9.3 @@ -709,7 +709,8 @@
     9.4      val _ = List.app (Lexicon.report_token ctxt) toks;
     9.5  
     9.6      val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
     9.7 -    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
     9.8 +    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
     9.9 +      handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
    9.10      val len = length pts;
    9.11  
    9.12      val limit = Config.get ctxt ambiguity_limit;
    10.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Wed Sep 08 13:30:41 2010 +0100
    10.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Wed Sep 08 14:46:21 2010 +0200
    10.3 @@ -177,6 +177,7 @@
    10.4  end.shortcut=
    10.5  fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
    10.6  firstTime=false
    10.7 +foldPainter=Circle
    10.8  home.shortcut=
    10.9  insert-newline-indent.shortcut=
   10.10  insert-newline.shortcut=ENTER
   10.11 @@ -203,6 +204,7 @@
   10.12  view.fontsize=18
   10.13  view.fracFontMetrics=false
   10.14  view.gutter.fontsize=12
   10.15 +view.gutter.selectionAreaWidth=18
   10.16  view.height=787
   10.17  view.middleMousePaste=true
   10.18  view.showToolbar=false
    11.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Sep 08 13:30:41 2010 +0100
    11.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Sep 08 14:46:21 2010 +0200
    11.3 @@ -69,87 +69,6 @@
    11.4            case _ => false
    11.5          }
    11.6      }
    11.7 -
    11.8 -
    11.9 -    /* mapping to jEdit token types */
   11.10 -    // TODO: as properties or CSS style sheet
   11.11 -
   11.12 -    val command_style: Map[String, Byte] =
   11.13 -    {
   11.14 -      import Token._
   11.15 -      Map[String, Byte](
   11.16 -        Keyword.THY_END -> KEYWORD2,
   11.17 -        Keyword.THY_SCRIPT -> LABEL,
   11.18 -        Keyword.PRF_SCRIPT -> LABEL,
   11.19 -        Keyword.PRF_ASM -> KEYWORD3,
   11.20 -        Keyword.PRF_ASM_GOAL -> KEYWORD3
   11.21 -      ).withDefaultValue(KEYWORD1)
   11.22 -    }
   11.23 -
   11.24 -    val token_style: Map[String, Byte] =
   11.25 -    {
   11.26 -      import Token._
   11.27 -      Map[String, Byte](
   11.28 -        // logical entities
   11.29 -        Markup.TCLASS -> NULL,
   11.30 -        Markup.TYCON -> NULL,
   11.31 -        Markup.FIXED_DECL -> FUNCTION,
   11.32 -        Markup.FIXED -> NULL,
   11.33 -        Markup.CONST_DECL -> FUNCTION,
   11.34 -        Markup.CONST -> NULL,
   11.35 -        Markup.FACT_DECL -> FUNCTION,
   11.36 -        Markup.FACT -> NULL,
   11.37 -        Markup.DYNAMIC_FACT -> LABEL,
   11.38 -        Markup.LOCAL_FACT_DECL -> FUNCTION,
   11.39 -        Markup.LOCAL_FACT -> NULL,
   11.40 -        // inner syntax
   11.41 -        Markup.TFREE -> NULL,
   11.42 -        Markup.FREE -> NULL,
   11.43 -        Markup.TVAR -> NULL,
   11.44 -        Markup.SKOLEM -> NULL,
   11.45 -        Markup.BOUND -> NULL,
   11.46 -        Markup.VAR -> NULL,
   11.47 -        Markup.NUM -> DIGIT,
   11.48 -        Markup.FLOAT -> DIGIT,
   11.49 -        Markup.XNUM -> DIGIT,
   11.50 -        Markup.XSTR -> LITERAL4,
   11.51 -        Markup.LITERAL -> OPERATOR,
   11.52 -        Markup.INNER_COMMENT -> COMMENT1,
   11.53 -        Markup.SORT -> NULL,
   11.54 -        Markup.TYP -> NULL,
   11.55 -        Markup.TERM -> NULL,
   11.56 -        Markup.PROP -> NULL,
   11.57 -        Markup.ATTRIBUTE -> NULL,
   11.58 -        Markup.METHOD -> NULL,
   11.59 -        // ML syntax
   11.60 -        Markup.ML_KEYWORD -> KEYWORD1,
   11.61 -        Markup.ML_DELIMITER -> OPERATOR,
   11.62 -        Markup.ML_IDENT -> NULL,
   11.63 -        Markup.ML_TVAR -> NULL,
   11.64 -        Markup.ML_NUMERAL -> DIGIT,
   11.65 -        Markup.ML_CHAR -> LITERAL1,
   11.66 -        Markup.ML_STRING -> LITERAL1,
   11.67 -        Markup.ML_COMMENT -> COMMENT1,
   11.68 -        Markup.ML_MALFORMED -> INVALID,
   11.69 -        // embedded source text
   11.70 -        Markup.ML_SOURCE -> COMMENT3,
   11.71 -        Markup.DOC_SOURCE -> COMMENT3,
   11.72 -        Markup.ANTIQ -> COMMENT4,
   11.73 -        Markup.ML_ANTIQ -> COMMENT4,
   11.74 -        Markup.DOC_ANTIQ -> COMMENT4,
   11.75 -        // outer syntax
   11.76 -        Markup.KEYWORD -> KEYWORD2,
   11.77 -        Markup.OPERATOR -> OPERATOR,
   11.78 -        Markup.COMMAND -> KEYWORD1,
   11.79 -        Markup.IDENT -> NULL,
   11.80 -        Markup.VERBATIM -> COMMENT3,
   11.81 -        Markup.COMMENT -> COMMENT1,
   11.82 -        Markup.CONTROL -> COMMENT3,
   11.83 -        Markup.MALFORMED -> INVALID,
   11.84 -        Markup.STRING -> LITERAL3,
   11.85 -        Markup.ALTSTRING -> LITERAL1
   11.86 -      ).withDefaultValue(NULL)
   11.87 -    }
   11.88    }
   11.89  
   11.90  
   11.91 @@ -272,27 +191,18 @@
   11.92            handler.handleToken(line_segment, style, offset, length, context)
   11.93  
   11.94          val syntax = session.current_syntax()
   11.95 -        val token_markup: PartialFunction[Text.Info[Any], Byte] =
   11.96 -        {
   11.97 -          case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
   11.98 -          if syntax.keyword_kind(name).isDefined =>
   11.99 -            Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
  11.100 -
  11.101 -          case Text.Info(_, XML.Elem(Markup(name, _), _))
  11.102 -          if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
  11.103 -            Document_Model.Token_Markup.token_style(name)
  11.104 -        }
  11.105 +        val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
  11.106  
  11.107          var last = start
  11.108 -        for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
  11.109 +        for (token <- tokens.iterator) {
  11.110            val Text.Range(token_start, token_stop) = token.range
  11.111            if (last < token_start)
  11.112              handle_token(Token.COMMENT1, last - start, token_start - last)
  11.113 -          handle_token(token.info, token_start - start, token_stop - token_start)
  11.114 +          handle_token(token.info getOrElse Token.NULL,
  11.115 +            token_start - start, token_stop - token_start)
  11.116            last = token_stop
  11.117          }
  11.118 -        if (last < stop)
  11.119 -          handle_token(Token.COMMENT1, last - start, stop - last)
  11.120 +        if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
  11.121  
  11.122          handle_token(Token.END, line_segment.count, 0)
  11.123          handler.setLineContext(context)
    12.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed Sep 08 13:30:41 2010 +0100
    12.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Wed Sep 08 14:46:21 2010 +0200
    12.3 @@ -13,42 +13,19 @@
    12.4  import scala.actors.Actor._
    12.5  
    12.6  import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
    12.7 -import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
    12.8 +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
    12.9  import javax.swing.{JPanel, ToolTipManager}
   12.10  import javax.swing.event.{CaretListener, CaretEvent}
   12.11  
   12.12 -import org.gjt.sp.jedit.OperatingSystem
   12.13 +import org.gjt.sp.jedit.{jEdit, OperatingSystem}
   12.14  import org.gjt.sp.jedit.gui.RolloverButton
   12.15 +import org.gjt.sp.jedit.options.GutterOptionPane
   12.16  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
   12.17  import org.gjt.sp.jedit.syntax.SyntaxStyle
   12.18  
   12.19  
   12.20  object Document_View
   12.21  {
   12.22 -  /* physical rendering */
   12.23 -
   12.24 -  def status_color(snapshot: Document.Snapshot, command: Command): Color =
   12.25 -  {
   12.26 -    val state = snapshot.state(command)
   12.27 -    if (snapshot.is_outdated) new Color(240, 240, 240)
   12.28 -    else
   12.29 -      Isar_Document.command_status(state.status) match {
   12.30 -        case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
   12.31 -        case Isar_Document.Finished => new Color(234, 248, 255)
   12.32 -        case Isar_Document.Failed => new Color(255, 193, 193)
   12.33 -        case Isar_Document.Unprocessed => new Color(255, 228, 225)
   12.34 -        case _ => Color.red
   12.35 -      }
   12.36 -  }
   12.37 -
   12.38 -  val message_markup: PartialFunction[Text.Info[Any], Color] =
   12.39 -  {
   12.40 -    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
   12.41 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
   12.42 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
   12.43 -  }
   12.44 -
   12.45 -
   12.46    /* document view of text area */
   12.47  
   12.48    private val key = new Object
   12.49 @@ -171,19 +148,17 @@
   12.50  
   12.51    /* subexpression highlighting */
   12.52  
   12.53 -  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
   12.54 +  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
   12.55 +    : Option[(Text.Range, Color)] =
   12.56    {
   12.57 -    val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
   12.58 -    {
   12.59 -      case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
   12.60 -        Some(snapshot.convert(range))
   12.61 +    val offset = text_area.xyToOffset(x, y)
   12.62 +    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
   12.63 +      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   12.64 +      case _ => None
   12.65      }
   12.66 -    val offset = text_area.xyToOffset(x, y)
   12.67 -    val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
   12.68 -    if (markup.hasNext) markup.next.info else None
   12.69    }
   12.70  
   12.71 -  private var highlight_range: Option[Text.Range] = None
   12.72 +  private var highlight_range: Option[(Text.Range, Color)] = None
   12.73  
   12.74    private val focus_listener = new FocusAdapter {
   12.75      override def focusLost(e: FocusEvent) { highlight_range = None }
   12.76 @@ -195,10 +170,10 @@
   12.77        if (!model.buffer.isLoaded) highlight_range = None
   12.78        else
   12.79          Isabelle.swing_buffer_lock(model.buffer) {
   12.80 -          highlight_range.map(invalidate_line_range(_))
   12.81 +          highlight_range map { case (range, _) => invalidate_line_range(range) }
   12.82            highlight_range =
   12.83              if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
   12.84 -          highlight_range.map(invalidate_line_range(_))
   12.85 +          highlight_range map { case (range, _) => invalidate_line_range(range) }
   12.86          }
   12.87      }
   12.88    }
   12.89 @@ -217,53 +192,70 @@
   12.90          val saved_color = gfx.getColor
   12.91          val ascent = text_area.getPainter.getFontMetrics.getAscent
   12.92  
   12.93 -        try {
   12.94 -          for (i <- 0 until physical_lines.length) {
   12.95 -            if (physical_lines(i) != -1) {
   12.96 -              val line_range = proper_line_range(start(i), end(i))
   12.97 +        for (i <- 0 until physical_lines.length) {
   12.98 +          if (physical_lines(i) != -1) {
   12.99 +            val line_range = proper_line_range(start(i), end(i))
  12.100  
  12.101 -              // background color
  12.102 -              val cmds = snapshot.node.command_range(snapshot.revert(line_range))
  12.103 -              for {
  12.104 -                (command, command_start) <- cmds if !command.is_ignored
  12.105 -                val range = line_range.restrict(snapshot.convert(command.range + command_start))
  12.106 -                r <- Isabelle.gfx_range(text_area, range)
  12.107 -              } {
  12.108 -                gfx.setColor(Document_View.status_color(snapshot, command))
  12.109 -                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
  12.110 -              }
  12.111 +            // background color: status
  12.112 +            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
  12.113 +            for {
  12.114 +              (command, command_start) <- cmds if !command.is_ignored
  12.115 +              val range = line_range.restrict(snapshot.convert(command.range + command_start))
  12.116 +              r <- Isabelle.gfx_range(text_area, range)
  12.117 +              color <- Isabelle_Markup.status_color(snapshot, command)
  12.118 +            } {
  12.119 +              gfx.setColor(color)
  12.120 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
  12.121 +            }
  12.122 +
  12.123 +            // background color: markup
  12.124 +            for {
  12.125 +              Text.Info(range, Some(color)) <-
  12.126 +                snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
  12.127 +              r <- Isabelle.gfx_range(text_area, range)
  12.128 +            } {
  12.129 +              gfx.setColor(color)
  12.130 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
  12.131 +            }
  12.132  
  12.133 -              // subexpression highlighting -- potentially from other snapshot
  12.134 -              if (highlight_range.isDefined) {
  12.135 -                if (line_range.overlaps(highlight_range.get)) {
  12.136 -                  Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
  12.137 -                    case None =>
  12.138 -                    case Some(r) =>
  12.139 -                      gfx.setColor(Color.black)
  12.140 -                      gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
  12.141 -                  }
  12.142 +            // sub-expression highlighting -- potentially from other snapshot
  12.143 +            highlight_range match {
  12.144 +              case Some((range, color)) if line_range.overlaps(range) =>
  12.145 +                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
  12.146 +                  case None =>
  12.147 +                  case Some(r) =>
  12.148 +                    gfx.setColor(color)
  12.149 +                    gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
  12.150                  }
  12.151 -              }
  12.152 +              case _ =>
  12.153 +            }
  12.154  
  12.155 -              // squiggly underline
  12.156 -              for {
  12.157 -                Text.Info(range, color) <-
  12.158 -                  snapshot.select_markup(line_range)(Document_View.message_markup)(null)
  12.159 -                if color != null
  12.160 -                r <- Isabelle.gfx_range(text_area, range)
  12.161 -              } {
  12.162 -                gfx.setColor(color)
  12.163 -                val x0 = (r.x / 2) * 2
  12.164 -                val y0 = r.y + ascent + 1
  12.165 -                for (x1 <- Range(x0, x0 + r.length, 2)) {
  12.166 -                  val y1 = if (x1 % 4 < 2) y0 else y0 + 1
  12.167 -                  gfx.drawLine(x1, y1, x1 + 1, y1)
  12.168 -                }
  12.169 +            // boxed text
  12.170 +            for {
  12.171 +              Text.Info(range, Some(color)) <-
  12.172 +                snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
  12.173 +              r <- Isabelle.gfx_range(text_area, range)
  12.174 +            } {
  12.175 +              gfx.setColor(color)
  12.176 +              gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
  12.177 +            }
  12.178 +
  12.179 +            // squiggly underline
  12.180 +            for {
  12.181 +              Text.Info(range, Some(color)) <-
  12.182 +                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
  12.183 +              r <- Isabelle.gfx_range(text_area, range)
  12.184 +            } {
  12.185 +              gfx.setColor(color)
  12.186 +              val x0 = (r.x / 2) * 2
  12.187 +              val y0 = r.y + ascent + 1
  12.188 +              for (x1 <- Range(x0, x0 + r.length, 2)) {
  12.189 +                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
  12.190 +                gfx.drawLine(x1, y1, x1 + 1, y1)
  12.191                }
  12.192              }
  12.193            }
  12.194          }
  12.195 -        finally { gfx.setColor(saved_color) }
  12.196        }
  12.197      }
  12.198  
  12.199 @@ -272,12 +264,52 @@
  12.200        Isabelle.swing_buffer_lock(model.buffer) {
  12.201          val snapshot = model.snapshot()
  12.202          val offset = text_area.xyToOffset(x, y)
  12.203 -        val markup =
  12.204 -          snapshot.select_markup(Text.Range(offset, offset + 1)) {
  12.205 -            case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
  12.206 -              Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
  12.207 -          } { null }
  12.208 -        if (markup.hasNext) markup.next.info else null
  12.209 +        snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
  12.210 +        {
  12.211 +          case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
  12.212 +          case _ => null
  12.213 +        }
  12.214 +      }
  12.215 +    }
  12.216 +  }
  12.217 +
  12.218 +
  12.219 +  /* gutter_extension */
  12.220 +
  12.221 +  private val gutter_extension = new TextAreaExtension
  12.222 +  {
  12.223 +    override def paintScreenLineRange(gfx: Graphics2D,
  12.224 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
  12.225 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
  12.226 +    {
  12.227 +      val gutter = text_area.getGutter
  12.228 +      val width = GutterOptionPane.getSelectionAreaWidth
  12.229 +      val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
  12.230 +      val FOLD_MARKER_SIZE = 12
  12.231 +
  12.232 +      if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
  12.233 +        Isabelle.swing_buffer_lock(model.buffer) {
  12.234 +          val snapshot = model.snapshot()
  12.235 +          for (i <- 0 until physical_lines.length) {
  12.236 +            if (physical_lines(i) != -1) {
  12.237 +              val line_range = proper_line_range(start(i), end(i))
  12.238 +
  12.239 +              // gutter icons
  12.240 +              val icons =
  12.241 +                (for (Text.Info(_, Some(icon)) <-
  12.242 +                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
  12.243 +                yield icon).toList.sortWith(_ >= _)
  12.244 +              icons match {
  12.245 +                case icon :: _ =>
  12.246 +                  val icn = icon.icon
  12.247 +                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
  12.248 +                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
  12.249 +                  icn.paintIcon(gutter, gfx, x0, y0)
  12.250 +                case Nil =>
  12.251 +              }
  12.252 +            }
  12.253 +          }
  12.254 +        }
  12.255        }
  12.256      }
  12.257    }
  12.258 @@ -328,13 +360,6 @@
  12.259        super.removeNotify
  12.260      }
  12.261  
  12.262 -    override def getToolTipText(event: MouseEvent): String =
  12.263 -    {
  12.264 -      val line = y_to_line(event.getY())
  12.265 -      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
  12.266 -      else ""
  12.267 -    }
  12.268 -
  12.269      override def paintComponent(gfx: Graphics)
  12.270      {
  12.271        super.paintComponent(gfx)
  12.272 @@ -342,18 +367,18 @@
  12.273        val buffer = model.buffer
  12.274        Isabelle.buffer_lock(buffer) {
  12.275          val snapshot = model.snapshot()
  12.276 -        val saved_color = gfx.getColor  // FIXME needed!?
  12.277 -        try {
  12.278 -          for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
  12.279 -            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
  12.280 -            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
  12.281 -            val y = line_to_y(line1)
  12.282 -            val height = HEIGHT * (line2 - line1)
  12.283 -            gfx.setColor(Document_View.status_color(snapshot, command))
  12.284 -            gfx.fillRect(0, y, getWidth - 1, height)
  12.285 -          }
  12.286 +        for {
  12.287 +          (command, start) <- snapshot.node.command_starts
  12.288 +          if !command.is_ignored
  12.289 +          val line1 = buffer.getLineOfOffset(snapshot.convert(start))
  12.290 +          val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
  12.291 +          val y = line_to_y(line1)
  12.292 +          val height = HEIGHT * (line2 - line1)
  12.293 +          color <- Isabelle_Markup.overview_color(snapshot, command)
  12.294 +        } {
  12.295 +          gfx.setColor(color)
  12.296 +          gfx.fillRect(0, y, getWidth - 1, height)
  12.297          }
  12.298 -        finally { gfx.setColor(saved_color) }
  12.299        }
  12.300      }
  12.301  
  12.302 @@ -371,6 +396,7 @@
  12.303    {
  12.304      text_area.getPainter.
  12.305        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
  12.306 +    text_area.getGutter.addExtension(gutter_extension)
  12.307      text_area.addFocusListener(focus_listener)
  12.308      text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
  12.309      text_area.addCaretListener(caret_listener)
  12.310 @@ -385,6 +411,7 @@
  12.311      text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
  12.312      text_area.removeCaretListener(caret_listener)
  12.313      text_area.removeLeftOfScrollBar(overview)
  12.314 +    text_area.getGutter.removeExtension(gutter_extension)
  12.315      text_area.getPainter.removeExtension(text_area_extension)
  12.316    }
  12.317  }
  12.318 \ No newline at end of file
    13.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Sep 08 13:30:41 2010 +0100
    13.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Sep 08 14:46:21 2010 +0200
    13.3 @@ -72,9 +72,11 @@
    13.4                        case _ => null
    13.5                      }
    13.6                  }
    13.7 -            } { null }
    13.8 -          if (markup.hasNext) markup.next.info else null
    13.9 -
   13.10 +            }
   13.11 +          markup match {
   13.12 +            case Text.Info(_, Some(link)) #:: _ => link
   13.13 +            case _ => null
   13.14 +          }
   13.15          case None => null
   13.16        }
   13.17      }
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Wed Sep 08 14:46:21 2010 +0200
    14.3 @@ -0,0 +1,198 @@
    14.4 +/*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
    14.5 +    Author:     Makarius
    14.6 +
    14.7 +Isabelle specific physical rendering and markup selection.
    14.8 +*/
    14.9 +
   14.10 +package isabelle.jedit
   14.11 +
   14.12 +
   14.13 +import isabelle._
   14.14 +
   14.15 +import java.awt.Color
   14.16 +
   14.17 +import org.gjt.sp.jedit.GUIUtilities
   14.18 +import org.gjt.sp.jedit.syntax.Token
   14.19 +
   14.20 +
   14.21 +object Isabelle_Markup
   14.22 +{
   14.23 +  /* physical rendering */
   14.24 +
   14.25 +  val outdated_color = new Color(240, 240, 240)
   14.26 +  val unfinished_color = new Color(255, 228, 225)
   14.27 +
   14.28 +  val regular_color = new Color(192, 192, 192)
   14.29 +  val warning_color = new Color(255, 168, 0)
   14.30 +  val error_color = new Color(255, 80, 80)
   14.31 +  val bad_color = new Color(255, 204, 153, 100)
   14.32 +
   14.33 +  class Icon(val priority: Int, val icon: javax.swing.Icon)
   14.34 +  {
   14.35 +    def >= (that: Icon): Boolean = this.priority >= that.priority
   14.36 +  }
   14.37 +  val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
   14.38 +  val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
   14.39 +
   14.40 +
   14.41 +  /* command status */
   14.42 +
   14.43 +  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   14.44 +  {
   14.45 +    val state = snapshot.state(command)
   14.46 +    if (snapshot.is_outdated) Some(outdated_color)
   14.47 +    else
   14.48 +      Isar_Document.command_status(state.status) match {
   14.49 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
   14.50 +        case Isar_Document.Unprocessed => Some(unfinished_color)
   14.51 +        case _ => None
   14.52 +      }
   14.53 +  }
   14.54 +
   14.55 +  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   14.56 +  {
   14.57 +    val state = snapshot.state(command)
   14.58 +    if (snapshot.is_outdated) None
   14.59 +    else
   14.60 +      Isar_Document.command_status(state.status) match {
   14.61 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
   14.62 +        case Isar_Document.Unprocessed => Some(unfinished_color)
   14.63 +        case Isar_Document.Failed => Some(error_color)
   14.64 +        case _ => None
   14.65 +      }
   14.66 +  }
   14.67 +
   14.68 +
   14.69 +  /* markup selectors */
   14.70 +
   14.71 +  private val subexp_include =
   14.72 +    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
   14.73 +
   14.74 +  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
   14.75 +  {
   14.76 +    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   14.77 +      (range, Color.black)
   14.78 +  }
   14.79 +
   14.80 +  val message: Markup_Tree.Select[Color] =
   14.81 +  {
   14.82 +    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
   14.83 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
   14.84 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   14.85 +  }
   14.86 +
   14.87 +  val gutter_message: Markup_Tree.Select[Icon] =
   14.88 +  {
   14.89 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
   14.90 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
   14.91 +  }
   14.92 +
   14.93 +  val background: Markup_Tree.Select[Color] =
   14.94 +  {
   14.95 +    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
   14.96 +  }
   14.97 +
   14.98 +  val box: Markup_Tree.Select[Color] =
   14.99 +  {
  14.100 +    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
  14.101 +  }
  14.102 +
  14.103 +  val tooltip: Markup_Tree.Select[String] =
  14.104 +  {
  14.105 +    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
  14.106 +      Pretty.string_of(List(Pretty.block(body)), margin = 40)
  14.107 +    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
  14.108 +    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
  14.109 +    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
  14.110 +    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
  14.111 +  }
  14.112 +
  14.113 +
  14.114 +  /* token markup -- text styles */
  14.115 +
  14.116 +  private val command_style: Map[String, Byte] =
  14.117 +  {
  14.118 +    import Token._
  14.119 +    Map[String, Byte](
  14.120 +      Keyword.THY_END -> KEYWORD2,
  14.121 +      Keyword.THY_SCRIPT -> LABEL,
  14.122 +      Keyword.PRF_SCRIPT -> LABEL,
  14.123 +      Keyword.PRF_ASM -> KEYWORD3,
  14.124 +      Keyword.PRF_ASM_GOAL -> KEYWORD3
  14.125 +    ).withDefaultValue(KEYWORD1)
  14.126 +  }
  14.127 +
  14.128 +  private val token_style: Map[String, Byte] =
  14.129 +  {
  14.130 +    import Token._
  14.131 +    Map[String, Byte](
  14.132 +      // logical entities
  14.133 +      Markup.TCLASS -> NULL,
  14.134 +      Markup.TYCON -> NULL,
  14.135 +      Markup.FIXED_DECL -> FUNCTION,
  14.136 +      Markup.FIXED -> NULL,
  14.137 +      Markup.CONST_DECL -> FUNCTION,
  14.138 +      Markup.CONST -> NULL,
  14.139 +      Markup.FACT_DECL -> FUNCTION,
  14.140 +      Markup.FACT -> NULL,
  14.141 +      Markup.DYNAMIC_FACT -> LABEL,
  14.142 +      Markup.LOCAL_FACT_DECL -> FUNCTION,
  14.143 +      Markup.LOCAL_FACT -> NULL,
  14.144 +      // inner syntax
  14.145 +      Markup.TFREE -> NULL,
  14.146 +      Markup.FREE -> NULL,
  14.147 +      Markup.TVAR -> NULL,
  14.148 +      Markup.SKOLEM -> NULL,
  14.149 +      Markup.BOUND -> NULL,
  14.150 +      Markup.VAR -> NULL,
  14.151 +      Markup.NUM -> DIGIT,
  14.152 +      Markup.FLOAT -> DIGIT,
  14.153 +      Markup.XNUM -> DIGIT,
  14.154 +      Markup.XSTR -> LITERAL4,
  14.155 +      Markup.LITERAL -> OPERATOR,
  14.156 +      Markup.INNER_COMMENT -> COMMENT1,
  14.157 +      Markup.SORT -> NULL,
  14.158 +      Markup.TYP -> NULL,
  14.159 +      Markup.TERM -> NULL,
  14.160 +      Markup.PROP -> NULL,
  14.161 +      Markup.ATTRIBUTE -> NULL,
  14.162 +      Markup.METHOD -> NULL,
  14.163 +      // ML syntax
  14.164 +      Markup.ML_KEYWORD -> KEYWORD1,
  14.165 +      Markup.ML_DELIMITER -> OPERATOR,
  14.166 +      Markup.ML_IDENT -> NULL,
  14.167 +      Markup.ML_TVAR -> NULL,
  14.168 +      Markup.ML_NUMERAL -> DIGIT,
  14.169 +      Markup.ML_CHAR -> LITERAL1,
  14.170 +      Markup.ML_STRING -> LITERAL1,
  14.171 +      Markup.ML_COMMENT -> COMMENT1,
  14.172 +      Markup.ML_MALFORMED -> INVALID,
  14.173 +      // embedded source text
  14.174 +      Markup.ML_SOURCE -> COMMENT3,
  14.175 +      Markup.DOC_SOURCE -> COMMENT3,
  14.176 +      Markup.ANTIQ -> COMMENT4,
  14.177 +      Markup.ML_ANTIQ -> COMMENT4,
  14.178 +      Markup.DOC_ANTIQ -> COMMENT4,
  14.179 +      // outer syntax
  14.180 +      Markup.KEYWORD -> KEYWORD2,
  14.181 +      Markup.OPERATOR -> OPERATOR,
  14.182 +      Markup.COMMAND -> KEYWORD1,
  14.183 +      Markup.IDENT -> NULL,
  14.184 +      Markup.VERBATIM -> COMMENT3,
  14.185 +      Markup.COMMENT -> COMMENT1,
  14.186 +      Markup.CONTROL -> COMMENT3,
  14.187 +      Markup.MALFORMED -> INVALID,
  14.188 +      Markup.STRING -> LITERAL3,
  14.189 +      Markup.ALTSTRING -> LITERAL1
  14.190 +    ).withDefaultValue(NULL)
  14.191 +  }
  14.192 +
  14.193 +  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
  14.194 +  {
  14.195 +    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
  14.196 +    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
  14.197 +
  14.198 +    case Text.Info(_, XML.Elem(Markup(name, _), _))
  14.199 +    if token_style(name) != Token.NULL => token_style(name)
  14.200 +  }
  14.201 +}
    15.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Sep 08 13:30:41 2010 +0100
    15.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Sep 08 14:46:21 2010 +0200
    15.3 @@ -286,10 +286,9 @@
    15.4      Isabelle.setup_tooltips()
    15.5    }
    15.6  
    15.7 -  override def stop()
    15.8 +  override def stop()  // FIXME fragile
    15.9    {
   15.10      Isabelle.session.stop()  // FIXME dialog!?
   15.11      Isabelle.session = null
   15.12 -    Isabelle.system = null
   15.13    }
   15.14  }