--- /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; }
+
--- 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; }
-
--- 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
--- 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";
--- 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"
--- 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 ||
--- 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)
}
}
}
--- 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 */
--- 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
--- 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")
--- 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;
--- 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)
}
--- 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)
--- 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) {