# HG changeset patch # User wenzelm # Date 1308403137 -7200 # Node ID e5dbf67b2a723a3471cc1c4d70215906cb369191 # Parent a666b8d11252d1bc61c21fcb73bc8e9c7ac2f346# Parent 55866987a7d9d63cc86aad7399e6e7ebd76127e1 merged diff -r a666b8d11252 -r e5dbf67b2a72 etc/isabelle.css --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/etc/isabelle.css Sat Jun 18 15:18:57 2011 +0200 @@ -0,0 +1,50 @@ +/* style file for Isabelle XHTML/XML output */ + +body { background-color: #FFFFFF; } + +.head { background-color: #FFFFFF; } +.source { background-color: #F0F0F0; padding: 10px; } + +.external_source { background-color: #F0F0F0; padding: 10px; } +.external_footer { background-color: #FFFFFF; } + +.theories { background-color: #F0F0F0; padding: 10px; } +.sessions { background-color: #F0F0F0; padding: 10px; } + +.name { font-style: italic; } +.filename { font-family: fixed; } + + +/* basic syntax markup */ + +.hidden, hidden { font-size: 0.1pt; visibility: hidden; } + +.tclass, tclass { color: red; } +.tfree, tfree { color: #A020F0; } +.tvar, tvar { color: #A020F0; } +.free, free { color: blue; } +.skolem, skolem { color: #D2691E; } +.bound, bound { color: green; } +.var, var { color: #00009B; } +.numeral, numeral { } +.literal, literal { font-weight: bold; } +.delimiter, delimiter { } +.inner_string, inner_string { color: #D2691E; } +.inner_comment, inner_comment { color: #8B0000; } + +.bold, bold { font-weight: bold; } +.loc, loc { color: #D2691E; } + +.keyword, keyword { font-weight: bold; } +.operator, operator { } +.command, command { font-weight: bold; } +.ident, ident { } +.string, string { color: #008B00; } +.altstring, altstring { color: #8B8B00; } +.verbatim, verbatim { color: #00008B; } +.comment, comment { color: #8B0000; } +.control, control { background-color: #FF6A6A; } +.malformed, malformed { background-color: #FF6A6A; } + +.malformed_span, malformed_span { background-color: #FF6A6A; } + diff -r a666b8d11252 -r e5dbf67b2a72 lib/html/isabelle.css --- a/lib/html/isabelle.css Fri Jun 17 20:38:43 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ -/* style file for Isabelle XHTML/XML output */ - -body { background-color: #FFFFFF; } - -.head { background-color: #FFFFFF; } -.source { background-color: #F0F0F0; padding: 10px; } - -.external_source { background-color: #F0F0F0; padding: 10px; } -.external_footer { background-color: #FFFFFF; } - -.theories { background-color: #F0F0F0; padding: 10px; } -.sessions { background-color: #F0F0F0; padding: 10px; } - -.name { font-style: italic; } -.filename { font-family: fixed; } - - -/* basic syntax markup */ - -.hidden, hidden { font-size: 0.1pt; visibility: hidden; } - -.tclass, tclass { color: red; } -.tfree, tfree { color: #A020F0; } -.tvar, tvar { color: #A020F0; } -.free, free { color: blue; } -.skolem, skolem { color: #D2691E; } -.bound, bound { color: green; } -.var, var { color: #00009B; } -.numeral, numeral { } -.literal, literal { font-weight: bold; } -.inner_string, inner_string { color: #D2691E; } -.inner_comment, inner_comment { color: #8B0000; } - -.bold, bold { font-weight: bold; } -.loc, loc { color: #D2691E; } - -.keyword, keyword { font-weight: bold; } -.operator, operator { } -.command, command { font-weight: bold; } -.ident, ident { } -.string, string { color: #008B00; } -.altstring, altstring { color: #8B8B00; } -.verbatim, verbatim { color: #00008B; } -.comment, comment { color: #8B0000; } -.control, control { background-color: #FF6A6A; } -.malformed, malformed { background-color: #FF6A6A; } - -.malformed_span, malformed_span { background-color: #FF6A6A; } - diff -r a666b8d11252 -r e5dbf67b2a72 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Fri Jun 17 20:38:43 2011 +0200 +++ b/src/HOL/Unix/Unix.thy Sat Jun 18 15:18:57 2011 +0200 @@ -847,7 +847,7 @@ The following invariant over the root file-system describes the bogus situation in an abstract manner: located at a certain @{term path} within the file-system is a non-empty directory that is - neither owned and nor writable by @{term user\<^isub>1}. + neither owned nor writable by @{term user\<^isub>1}. *} definition diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/General/markup.ML Sat Jun 18 15:18:57 2011 +0200 @@ -47,6 +47,7 @@ val varN: string val var: T val numeralN: string val numeral: T val literalN: string val literal: T + val delimiterN: string val delimiter: T val inner_stringN: string val inner_string: T val inner_commentN: string val inner_comment: T val token_rangeN: string val token_range: T @@ -223,6 +224,7 @@ val (varN, var) = markup_elem "var"; val (numeralN, numeral) = markup_elem "numeral"; val (literalN, literal) = markup_elem "literal"; +val (delimiterN, delimiter) = markup_elem "delimiter"; val (inner_stringN, inner_string) = markup_elem "inner_string"; val (inner_commentN, inner_comment) = markup_elem "inner_comment"; diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/General/markup.scala Sat Jun 18 15:18:57 2011 +0200 @@ -167,6 +167,7 @@ val XNUM = "xnum" val XSTR = "xstr" val LITERAL = "literal" + val DELIMITER = "delimiter" val INNER_STRING = "inner_string" val INNER_COMMENT = "inner_comment" diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/Isar/token.scala Sat Jun 18 15:18:57 2011 +0200 @@ -64,7 +64,7 @@ sealed case class Token(val kind: Token.Kind.Value, val source: String) { def is_command: Boolean = kind == Token.Kind.COMMAND - def is_keyword: Boolean = kind == Token.Kind.KEYWORD + def is_operator: Boolean = kind == Token.Kind.KEYWORD && !Symbol.is_ascii_identifier(source) def is_delimited: Boolean = kind == Token.Kind.STRING || kind == Token.Kind.ALT_STRING || diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/PIDE/document.scala Sat Jun 18 15:18:57 2011 +0200 @@ -307,20 +307,8 @@ def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - - def convert(range: Text.Range): Text.Range = - try { if (edits.isEmpty) range else range.map(convert(_)) } - catch { // FIXME tmp - case e: IllegalArgumentException => - System.err.println((true, range, edits)); throw(e) - } - - def revert(range: Text.Range): Text.Range = - try { if (edits.isEmpty) range else range.map(revert(_)) } - catch { // FIXME tmp - case e: IllegalArgumentException => - System.err.println((false, range, reverse_edits)); throw(e) - } + def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r)) + def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r)) def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) : Stream[Text.Info[Option[A]]] = @@ -334,9 +322,7 @@ if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) => result(Text.Info(convert(r0 + command_start), info)) } - val r = convert(r0 + command_start) - if !r.is_singularity - } yield Text.Info(r, x) + } yield Text.Info(convert(r0 + command_start), x) } } } diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/PIDE/text.scala Sat Jun 18 15:18:57 2011 +0200 @@ -25,7 +25,8 @@ sealed case class Range(val start: Offset, val stop: Offset) { // denotation: {start} Un {i. start < i & i < stop} - require(start <= stop) + if (start > stop) + error("Bad range: [" + start.toString + ":" + stop.toString + "]") override def toString = "[" + start.toString + ":" + stop.toString + "]" @@ -42,6 +43,10 @@ def restrict(that: Range): Range = Range(this.start max that.start, this.stop min that.stop) + + def try_restrict(that: Range): Option[Range] = + try { Some (restrict(that)) } + catch { case _: RuntimeException => None } } @@ -50,6 +55,9 @@ case class Info[A](val range: Text.Range, val info: A) { def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) + def try_restrict(r: Text.Range): Option[Info[A]] = + try { Some(Info(range.restrict(r), info)) } + catch { case _: RuntimeException => None } } @@ -71,11 +79,13 @@ private def transform(do_insert: Boolean, i: Offset): Offset = if (i < start) i - else if (is_insert == do_insert) i + text.length + else if (do_insert) i + text.length else (i - text.length) max start - def convert(i: Offset): Offset = transform(true, i) - def revert(i: Offset): Offset = transform(false, i) + def convert(i: Offset): Offset = transform(is_insert, i) + def revert(i: Offset): Offset = transform(!is_insert, i) + def convert(range: Range): Range = range.map(convert) + def revert(range: Range): Range = range.map(revert) /* edit strings */ diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/Syntax/lexicon.ML Sat Jun 18 15:18:57 2011 +0200 @@ -203,8 +203,11 @@ | Comment => Markup.inner_comment | EOF => Markup.empty; -fun report_token ctxt (Token (kind, _, (pos, _))) = - Context_Position.report ctxt pos (token_kind_markup kind); +fun report_token ctxt (Token (kind, s, (pos, _))) = + let val markup = + if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter + else token_kind_markup kind + in Context_Position.report ctxt pos markup end; fun reported_token_range ctxt tok = if is_proper tok diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/Thy/present.ML Sat Jun 18 15:18:57 2011 +0200 @@ -400,7 +400,7 @@ File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) (HTML.applet_pages name (Url.File index_path, name)); - File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; + File.copy (Path.explode "~~/etc/isabelle.css") html_prefix; List.app finish_html thys; List.app (uncurry File.write) files; if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") diff -r a666b8d11252 -r e5dbf67b2a72 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.ML Sat Jun 18 15:18:57 2011 +0200 @@ -65,7 +65,7 @@ | Token.EOF => Markup.control; fun token_markup tok = - if Token.keyword_with (not o Lexicon.is_identifier) tok then Markup.operator + if Token.keyword_with (not o Lexicon.is_ascii_identifier) tok then Markup.operator else let val kind = Token.kind_of tok; diff -r a666b8d11252 -r e5dbf67b2a72 src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Sat Jun 18 15:18:57 2011 +0200 @@ -33,6 +33,8 @@ val bad_color = new Color(255, 106, 106, 100) val hilite_color = new Color(255, 204, 102, 100) + val subexp_color = new Color(0xC0, 0xC0, 0xC0, 100) + val keyword1_color = get_color("#006699") val keyword2_color = get_color("#009966") @@ -108,16 +110,11 @@ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color } - /* FIXME update - Markup.ML_SOURCE -> COMMENT3, - Markup.DOC_SOURCE -> COMMENT3, - Markup.ANTIQ -> COMMENT4, - Markup.ML_ANTIQ -> COMMENT4, - Markup.DOC_ANTIQ -> COMMENT4, - */ - - private val foreground_colors: Map[String, Color] = + private val text_colors: Map[String, Color] = Map( + Markup.LITERAL -> keyword1_color, + Markup.DELIMITER -> get_color("black"), + Markup.IDENT -> get_color("black"), Markup.TCLASS -> get_color("red"), Markup.TFREE -> get_color("#A020F0"), Markup.TVAR -> get_color("#A020F0"), @@ -129,50 +126,56 @@ Markup.INNER_STRING -> get_color("#D2691E"), Markup.INNER_COMMENT -> get_color("#8B0000"), Markup.DYNAMIC_FACT -> get_color("yellowgreen"), - Markup.LITERAL -> keyword1_color, Markup.ML_KEYWORD -> keyword1_color, Markup.ML_DELIMITER -> get_color("black"), Markup.ML_NUMERAL -> get_color("red"), Markup.ML_CHAR -> get_color("#D2691E"), Markup.ML_STRING -> get_color("#D2691E"), Markup.ML_COMMENT -> get_color("#8B0000"), - Markup.ML_MALFORMED -> get_color("#FF6A6A") - ) + Markup.ML_MALFORMED -> get_color("#FF6A6A"), + Markup.ANTIQ -> get_color("blue")) - val foreground: Markup_Tree.Select[Color] = + val text_color: Markup_Tree.Select[Color] = { case Text.Info(_, XML.Elem(Markup(m, _), _)) - if foreground_colors.isDefinedAt(m) => foreground_colors(m) + if text_colors.isDefinedAt(m) => text_colors(m) } + private val tooltips: Map[String, String] = + Map( + Markup.SORT -> "sort", + Markup.TYP -> "type", + Markup.TERM -> "term", + Markup.PROP -> "proposition", + Markup.TOKEN_RANGE -> "inner syntax token", + Markup.FREE -> "free variable (globally fixed)", + Markup.SKOLEM -> "skolem variable (locally fixed)", + Markup.BOUND -> "bound variable (internally fixed)", + Markup.VAR -> "schematic variable", + Markup.TFREE -> "free type variable", + Markup.TVAR -> "schematic type variable", + Markup.ML_SOURCE -> "ML source", + Markup.DOC_SOURCE -> "document source") + val tooltip: Markup_Tree.Select[String] = { case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = Isabelle.Int_Property("tooltip-margin")) - case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort" - case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type" - case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term" - case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition" - case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token" - case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)" - case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)" - case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)" - case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable" - case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable" - case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable" + case Text.Info(_, XML.Elem(Markup(name, _), _)) + if tooltips.isDefinedAt(name) => tooltips(name) } private val subexp_include = Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, - Markup.TFREE, Markup.TVAR) + Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE) val subexp: Markup_Tree.Select[(Text.Range, Color)] = { case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => - (range, Color.black) + (range, subexp_color) } @@ -203,8 +206,8 @@ Token.Kind.TYPE_VAR -> NULL, Token.Kind.NAT -> NULL, Token.Kind.FLOAT -> NULL, - Token.Kind.STRING -> LITERAL3, - Token.Kind.ALT_STRING -> LITERAL1, + Token.Kind.STRING -> LITERAL1, + Token.Kind.ALT_STRING -> LITERAL2, Token.Kind.VERBATIM -> COMMENT3, Token.Kind.SPACE -> NULL, Token.Kind.COMMENT -> COMMENT1, @@ -213,9 +216,7 @@ } def token_markup(syntax: Outer_Syntax, token: Token): Byte = - if (token.is_command) - command_style(syntax.keyword_kind(token.content).getOrElse("")) - else if (token.is_keyword && !Symbol.is_ascii_identifier(token.content)) - JEditToken.OPERATOR + if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) + else if (token.is_operator) JEditToken.OPERATOR else token_style(token.kind) } diff -r a666b8d11252 -r e5dbf67b2a72 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Sat Jun 18 15:18:57 2011 +0200 @@ -90,10 +90,10 @@ val line_range = doc_view.proper_line_range(start(i), end(i)) // background color: status - val cmds = snapshot.node.command_range(snapshot.revert(line_range)) for { - (command, command_start) <- cmds if !command.is_ignored - val range = line_range.restrict(snapshot.convert(command.range + command_start)) + (command, command_start) <- snapshot.node.command_range(snapshot.revert(line_range)) + if !command.is_ignored + range <- line_range.try_restrict(snapshot.convert(command.range + command_start)) r <- Isabelle.gfx_range(text_area, range) color <- Isabelle_Markup.status_color(snapshot, command) } { @@ -121,18 +121,6 @@ gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4) } - // sub-expression highlighting -- potentially from other snapshot - doc_view.highlight_range match { - case Some((range, color)) if line_range.overlaps(range) => - Isabelle.gfx_range(text_area, line_range.restrict(range)) match { - case None => - case Some(r) => - gfx.setColor(color) - gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) - } - case _ => - } - // squiggly underline for { Text.Info(range, Some(color)) <- @@ -219,7 +207,11 @@ val chunk_font = chunk.style.getFont val chunk_color = chunk.style.getForegroundColor - val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground) + val markup = + for { + x <- painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.text_color) + y <- x.try_restrict(chunk_range) + } yield y gfx.setFont(chunk_font) if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null && @@ -228,14 +220,16 @@ gfx.setColor(chunk_color) gfx.drawGlyphVector(chunk.gv, x + w, y) } - else { + else if (!markup.isEmpty) { var x1 = x + w - for (Text.Info(range, info) <- markup) { - // FIXME proper range!? - val str = - chunk.str.substring( - (range.start - chunk_offset) max 0, - (range.stop - chunk_offset) min chunk_length) + for { + Text.Info(range, info) <- + Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++ + markup.iterator ++ + Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None)) + if !range.is_singularity + } { + val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset) gfx.setColor(info.getOrElse(chunk_color)) if (range.contains(caret_offset)) { val astr = new AttributedString(str) @@ -298,6 +292,39 @@ } + /* foreground */ + + private val foreground_painter = new TextAreaExtension + { + override def paintScreenLineRange(gfx: Graphics2D, + first_line: Int, last_line: Int, physical_lines: Array[Int], + start: Array[Int], end: Array[Int], y: Int, line_height: Int) + { + doc_view.robust_body(()) { + val snapshot = painter_snapshot + + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + val line_range = doc_view.proper_line_range(start(i), end(i)) + + // highlighted range -- potentially from other snapshot + doc_view.highlight_range match { + case Some((range, color)) if line_range.overlaps(range) => + Isabelle.gfx_range(text_area, line_range.restrict(range)) match { + case None => + case Some(r) => + gfx.setColor(color) + gfx.fillRect(r.x, y + i * line_height, r.length, line_height) + } + case _ => + } + } + } + } + } + } + + /* caret -- outside of text range */ private class Caret_Painter(before: Boolean) extends TextAreaExtension @@ -353,6 +380,7 @@ painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2) painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter) + painter.addExtension(500, foreground_painter) painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state) painter.removeExtension(orig_text_painter) } @@ -362,6 +390,7 @@ val painter = text_area.getPainter painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) painter.removeExtension(reset_state) + painter.removeExtension(foreground_painter) painter.removeExtension(caret_painter) painter.removeExtension(after_caret_painter2) painter.removeExtension(before_caret_painter2) diff -r a666b8d11252 -r e5dbf67b2a72 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Fri Jun 17 20:38:43 2011 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Sat Jun 18 15:18:57 2011 +0200 @@ -30,8 +30,8 @@ private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN") - private class Line_Context(val context: Scan.Context, prev: Line_Context) - extends TokenMarker.LineContext(isabelle_rules, prev) + private class Line_Context(val context: Scan.Context) + extends TokenMarker.LineContext(isabelle_rules, null) { override def hashCode: Int = context.hashCode override def equals(that: Any): Boolean = @@ -43,16 +43,17 @@ def token_marker(session: Session, buffer: Buffer): TokenMarker = new TokenMarker { - override def markTokens(raw_context: TokenMarker.LineContext, + override def markTokens(context: TokenMarker.LineContext, handler: TokenHandler, line: Segment): TokenMarker.LineContext = { val syntax = session.current_syntax() - - val context = raw_context.asInstanceOf[Line_Context] - val ctxt = if (context == null) Scan.Finished else context.context - + val ctxt = + context match { + case c: Line_Context => c.context + case _ => Scan.Finished + } val (tokens, ctxt1) = syntax.scan_context(line, ctxt) - val context1 = new Line_Context(ctxt1, context) + val context1 = new Line_Context(ctxt1) var offset = 0 for (token <- tokens) {