improved handling of extended styles and hard tabs when prover is inactive;
authorwenzelm
Sun Sep 04 17:35:34 2011 +0200 (2011-09-04)
changeset 44702eb00752507c7
parent 44701 0fd2bf8eaa9f
child 44703 f2bfe19239bc
improved handling of extended styles and hard tabs when prover is inactive;
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 17:21:11 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 04 17:35:34 2011 +0200
     1.3 @@ -173,42 +173,42 @@
     1.4            case _ => Some(Scan.Finished)
     1.5          }
     1.6        val context1 =
     1.7 -        if (line_ctxt.isDefined && Isabelle.session.is_ready) {
     1.8 -          val syntax = Isabelle.session.current_syntax()
     1.9 -    
    1.10 -          val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
    1.11 -          val context1 = new Line_Context(Some(ctxt1))
    1.12 -    
    1.13 -          val extended = extended_styles(line)
    1.14 -    
    1.15 -          var offset = 0
    1.16 -          for (token <- tokens) {
    1.17 -            val style = Isabelle_Markup.token_markup(syntax, token)
    1.18 -            val length = token.source.length
    1.19 -            val end_offset = offset + length
    1.20 -            if ((offset until end_offset) exists
    1.21 -                (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
    1.22 -              for (i <- offset until end_offset) {
    1.23 -                val style1 =
    1.24 -                  extended.get(i) match {
    1.25 -                    case None => style
    1.26 -                    case Some(ext) => ext(style)
    1.27 -                  }
    1.28 -                handler.handleToken(line, style1, i, 1, context1)
    1.29 -              }
    1.30 +      {
    1.31 +        val (styled_tokens, context1) =
    1.32 +          if (line_ctxt.isDefined && Isabelle.session.is_ready) {
    1.33 +            val syntax = Isabelle.session.current_syntax()
    1.34 +            val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
    1.35 +            val styled_tokens = tokens.map(tok => (Isabelle_Markup.token_markup(syntax, tok), tok))
    1.36 +            (styled_tokens, new Line_Context(Some(ctxt1)))
    1.37 +          }
    1.38 +          else {
    1.39 +            val token = Token(Token.Kind.UNPARSED, line.subSequence(0, line.count).toString)
    1.40 +            (List((JEditToken.NULL, token)), new Line_Context(None))
    1.41 +          }
    1.42 +
    1.43 +        val extended = extended_styles(line)
    1.44 +
    1.45 +        var offset = 0
    1.46 +        for ((style, token) <- styled_tokens) {
    1.47 +          val length = token.source.length
    1.48 +          val end_offset = offset + length
    1.49 +          if ((offset until end_offset) exists
    1.50 +              (i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
    1.51 +            for (i <- offset until end_offset) {
    1.52 +              val style1 =
    1.53 +                extended.get(i) match {
    1.54 +                  case None => style
    1.55 +                  case Some(ext) => ext(style)
    1.56 +                }
    1.57 +              handler.handleToken(line, style1, i, 1, context1)
    1.58              }
    1.59 -            else handler.handleToken(line, style, offset, length, context1)
    1.60 -            offset += length
    1.61            }
    1.62 -          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    1.63 -          context1
    1.64 +          else handler.handleToken(line, style, offset, length, context1)
    1.65 +          offset += length
    1.66          }
    1.67 -        else {
    1.68 -          val context1 = new Line_Context(None)
    1.69 -          handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
    1.70 -          handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    1.71 -          context1
    1.72 -        }
    1.73 +        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    1.74 +        context1
    1.75 +      }
    1.76        val context2 = context1.intern
    1.77        handler.setLineContext(context2)
    1.78        context2