# HG changeset patch # User wenzelm # Date 1392569413 -3600 # Node ID a3870c12f254172d1daee474247d1be0e8afc85d # Parent bd67ebe275e0bdfb4ff26606b6e1a8b166a67439# Parent d0157612ebe588bbeab8c94d817c45b3e5b6f673 merged diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/General/antiquote.ML Sun Feb 16 17:50:13 2014 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/General/antiquote.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius -Text with antiquotations of inner items (types, terms, theorems etc.). +Antiquotations within plain text. *) signature ANTIQUOTE = @@ -13,7 +13,7 @@ val reports_of: ('a -> Position.report_text list) -> 'a antiquote list -> Position.report_text list val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list - val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list + val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list end; @@ -45,10 +45,10 @@ val err_prefix = "Antiquotation lexical error: "; val scan_txt = - $$$ "@" --| Scan.ahead (~$$ "{") || - Scan.one (fn (s, _) => s <> "@" andalso Symbol.is_regular s) >> single; + Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") || + Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.is_regular s)) >> flat; -val scan_ant = +val scan_antiq_body = Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; @@ -58,10 +58,10 @@ val scan_antiq = Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") - (Scan.repeat scan_ant -- ($$ "}" |-- Symbol_Pos.scan_pos))) + (Scan.repeat scan_antiq_body -- ($$ "}" |-- Symbol_Pos.scan_pos))) >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); -val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat); +val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text; end; @@ -69,7 +69,7 @@ (* read *) fun read (syms, pos) = - (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of + (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of SOME xs => (Position.reports_text (reports_of (K []) xs); xs) | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos)); diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/General/antiquote.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/antiquote.scala Sun Feb 16 17:50:13 2014 +0100 @@ -0,0 +1,55 @@ +/* Title: Pure/ML/antiquote.scala + Author: Makarius + +Antiquotations within plain text. +*/ + +package isabelle + + +import scala.util.parsing.input.CharSequenceReader + + +object Antiquote +{ + sealed abstract class Antiquote + case class Text(source: String) extends Antiquote + case class Antiq(source: String) extends Antiquote + + + /* parsers */ + + object Parsers extends Parsers + + trait Parsers extends Scan.Parsers + { + private val txt: Parser[String] = + rep1("@" ~ guard(one(s => s != "{")) | many1(s => s != "@")) ^^ (x => x.mkString) + + val antiq_other: Parser[String] = + many1(s => s != "\"" && s != "`" && s != "}" && !Symbol.is_open(s) && !Symbol.is_close(s)) + + private val antiq_body: Parser[String] = + quoted("\"") | (quoted("`") | (cartouche | antiq_other)) + + val antiq: Parser[String] = + "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z } + + val antiquote: Parser[Antiquote] = + antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x)) + } + + + /* read */ + + def read(input: CharSequence): List[Antiquote] = + { + Parsers.parseAll(Parsers.rep(Parsers.antiquote), new CharSequenceReader(input)) match { + case Parsers.Success(xs, _) => xs + case Parsers.NoSuccess(_, next) => + error("Malformed quotation/antiquotation source" + + Position.here(Position.Line(next.pos.line))) + } + } +} + diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/General/scan.scala Sun Feb 16 17:50:13 2014 +0100 @@ -17,14 +17,14 @@ object Scan { - /** context of partial scans (line boundary) **/ + /** context of partial line-oriented scans **/ - abstract class Context - case object Finished extends Context - case class Quoted(quote: String) extends Context - case object Verbatim extends Context - case class Cartouche(depth: Int) extends Context - case class Comment(depth: Int) extends Context + abstract class Line_Context + case object Finished extends Line_Context + case class Quoted(quote: String) extends Line_Context + case object Verbatim extends Line_Context + case class Cartouche(depth: Int) extends Line_Context + case class Comment(depth: Int) extends Line_Context @@ -110,7 +110,7 @@ else body } - def quoted_context(quote: Symbol.Symbol, ctxt: Context): Parser[(String, Context)] = + def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] = { ctxt match { case Finished => @@ -123,7 +123,7 @@ case x ~ None => (x, ctxt) } case _ => failure("") } - }.named("quoted_context") + }.named("quoted_line") def recover_quoted(quote: Symbol.Symbol): Parser[String] = quote ~ quoted_body(quote) ^^ { case x ~ y => x + y } @@ -145,7 +145,7 @@ source.substring(2, source.length - 2) } - def verbatim_context(ctxt: Context): Parser[(String, Context)] = + def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { ctxt match { case Finished => @@ -158,7 +158,7 @@ case x ~ None => (x, Verbatim) } case _ => failure("") } - }.named("verbatim_context") + }.named("verbatim_line") val recover_verbatim: Parser[String] = "{*" ~ verbatim_body ^^ { case x ~ y => x + y } @@ -194,7 +194,7 @@ def cartouche: Parser[String] = cartouche_depth(0) ^? { case (x, d) if d == 0 => x } - def cartouche_context(ctxt: Context): Parser[(String, Context)] = + def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { val depth = ctxt match { @@ -258,7 +258,7 @@ def comment: Parser[String] = comment_depth(0) ^? { case (x, d) if d == 0 => x } - def comment_context(ctxt: Context): Parser[(String, Context)] = + def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { val depth = ctxt match { diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Sun Feb 16 17:50:13 2014 +0100 @@ -137,13 +137,13 @@ def scan(input: CharSequence): List[Token] = scan(new CharSequenceReader(input)) - def scan_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) = + def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) = { var in: Reader[Char] = new CharSequenceReader(input) val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { - Token.Parsers.parse(Token.Parsers.token_context(lexicon, is_command, ctxt), in) match { + Token.Parsers.parse(Token.Parsers.token_line(lexicon, is_command, ctxt), in) match { case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest } case Token.Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/Isar/token.scala Sun Feb 16 17:50:13 2014 +0100 @@ -26,7 +26,7 @@ val STRING = Value("string") val ALT_STRING = Value("back-quoted string") val VERBATIM = Value("verbatim text") - val CARTOUCHE = Value("cartouche") + val CARTOUCHE = Value("text cartouche") val SPACE = Value("white space") val COMMENT = Value("comment text") val ERROR = Value("bad input") @@ -102,16 +102,16 @@ def token(lexicon: Scan.Lexicon, is_command: String => Boolean): Parser[Token] = delimited_token | other_token(lexicon, is_command) - def token_context(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Context) - : Parser[(Token, Scan.Context)] = + def token_line(lexicon: Scan.Lexicon, is_command: String => Boolean, ctxt: Scan.Line_Context) + : Parser[(Token, Scan.Line_Context)] = { val string = - quoted_context("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) } + quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Token.Kind.STRING, x), c) } val alt_string = - quoted_context("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } - val verb = verbatim_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } - val cart = cartouche_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) } - val cmt = comment_context(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } + quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Token.Kind.ALT_STRING, x), c) } + val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } + val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) } + val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } val other = other_token(lexicon, is_command) ^^ { case x => (x, Scan.Finished) } string | (alt_string | (verb | (cart | (cmt | other)))) diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/ML/ml_lex.scala Sun Feb 16 17:50:13 2014 +0100 @@ -51,6 +51,13 @@ val STRING = Value("quoted string") val SPACE = Value("white space") val COMMENT = Value("comment text") + val ANTIQ = Value("antiquotation") + val ANTIQ_START = Value("antiquotation: start") + val ANTIQ_STOP = Value("antiquotation: stop") + val ANTIQ_OTHER = Value("antiquotation: other") + val ANTIQ_STRING = Value("antiquotation: quoted string") + val ANTIQ_ALT_STRING = Value("antiquotation: back-quoted string") + val ANTIQ_CARTOUCHE = Value("antiquotation: text cartouche") val ERROR = Value("bad input") } @@ -64,9 +71,10 @@ /** parsers **/ - case object ML_String extends Scan.Context + case object ML_String extends Scan.Line_Context + case class Antiq(ctxt: Scan.Line_Context) extends Scan.Line_Context - private object Parsers extends Scan.Parsers + private object Parsers extends Scan.Parsers with Antiquote.Parsers { /* string material */ @@ -107,9 +115,9 @@ private val ml_string: Parser[Token] = "\"" ~ ml_string_body ~ "\"" ^^ { case x ~ y ~ z => Token(Kind.STRING, x + y + z) } - private def ml_string_context(ctxt: Scan.Context): Parser[(Token, Scan.Context)] = + private def ml_string_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = { - def result(x: String, c: Scan.Context) = (Token(Kind.STRING, x), c) + def result(x: String, c: Scan.Line_Context) = (Token(Kind.STRING, x), c) ctxt match { case Scan.Finished => @@ -130,8 +138,8 @@ private val ml_comment: Parser[Token] = comment ^^ (x => Token(Kind.COMMENT, x)) - private def ml_comment_context(ctxt: Scan.Context): Parser[(Token, Scan.Context)] = - comment_context(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) } + private def ml_comment_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + comment_line(ctxt) ^^ { case (x, c) => (Token(Kind.COMMENT, x), c) } /* delimited token */ @@ -192,22 +200,52 @@ val keyword = literal(lexicon) ^^ (x => Token(Kind.KEYWORD, x)) + val ml_antiq = antiq ^^ (x => Token(Kind.ANTIQ, x)) + val bad = one(_ => true) ^^ (x => Token(Kind.ERROR, x)) - space | (recover_delimited | - (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad)) + space | (recover_delimited | (ml_antiq | + (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))) } + /* antiquotations (line-oriented) */ + + def ml_antiq_start(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + ctxt match { + case Scan.Finished => "@{" ^^ (x => (Token(Kind.ANTIQ_START, x), Antiq(Scan.Finished))) + case _ => failure("") + } + + def ml_antiq_stop(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + ctxt match { + case Antiq(Scan.Finished) => "}" ^^ (x => (Token(Kind.ANTIQ_STOP, x), Scan.Finished)) + case _ => failure("") + } + + def ml_antiq_body(context: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = + context match { + case Antiq(ctxt) => + (if (ctxt == Scan.Finished) antiq_other ^^ (x => (Token(Kind.ANTIQ_OTHER, x), context)) + else failure("")) | + quoted_line("\"", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_STRING, x), Antiq(c)) } | + quoted_line("`", ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_ALT_STRING, x), Antiq(c)) } | + cartouche_line(ctxt) ^^ { case (x, c) => (Token(Kind.ANTIQ_CARTOUCHE, x), Antiq(c)) } + case _ => failure("") + } + + /* token */ def token: Parser[Token] = delimited_token | other_token - def token_context(ctxt: Scan.Context): Parser[(Token, Scan.Context)] = + def token_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] = { val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished)) - ml_string_context(ctxt) | (ml_comment_context(ctxt) | other) + ml_string_line(ctxt) | + (ml_comment_line(ctxt) | + (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other)))) } } @@ -222,13 +260,14 @@ } } - def tokenize_context(input: CharSequence, context: Scan.Context): (List[Token], Scan.Context) = + def tokenize_line(input: CharSequence, context: Scan.Line_Context) + : (List[Token], Scan.Line_Context) = { var in: Reader[Char] = new CharSequenceReader(input) val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { - Parsers.parse(Parsers.token_context(ctxt), in) match { + Parsers.parse(Parsers.token_line(ctxt), in) match { case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest } case Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Sun Feb 16 17:50:13 2014 +0100 @@ -35,7 +35,7 @@ (* attribute source *) val _ = Theory.setup - (ML_Context.add_antiq (Binding.name "attributes") + (ML_Context.add_antiq @{binding attributes} (Scan.depend (fn context => Parse_Spec.attribs >> (fn raw_srcs => let val ctxt = Context.the_proof context; @@ -73,10 +73,10 @@ in (Context.Proof ctxt'', decl) end; val _ = Theory.setup - (ML_Context.add_antiq (Binding.name "thm") + (ML_Context.add_antiq @{binding thm} (Scan.depend (fn context => Scan.pass context Attrib.thm >> (thm_binding "thm" true context o single))) #> - ML_Context.add_antiq (Binding.name "thms") + ML_Context.add_antiq @{binding thms} (Scan.depend (fn context => Scan.pass context Attrib.thms >> thm_binding "thms" false context))); @@ -86,17 +86,24 @@ val and_ = Args.$$$ "and"; val by = Args.$$$ "by"; val goal = Scan.unless (by || and_) Args.name_inner_syntax; +val goals1 = Scan.repeat1 goal; val _ = Theory.setup - (ML_Context.add_antiq (Binding.name "lemma") + (ML_Context.add_antiq @{binding lemma} (Scan.depend (fn context => - Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) -- - (by |-- Method.parse -- Scan.option Method.parse) >> - (fn ((is_open, raw_propss), methods) => + Args.mode "open" -- goals1 -- Scan.repeat (Parse.position and_ -- Parse.!!! goals1) -- + (Parse.position by -- (Method.parse -- Scan.option Method.parse)) >> + (fn (((is_open, raw_props), and_propss), ((_, by_pos), methods)) => let val ctxt = Context.proof_of context; - val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; + val reports = + (by_pos, Markup.keyword1) :: + map (fn ((_, and_pos), _) => (and_pos, Markup.keyword2)) and_propss; + val _ = Context_Position.reports ctxt reports; + + val propss = + burrow (map (rpair []) o Syntax.read_props ctxt) (raw_props :: map #2 and_propss); val prep_result = Goal.norm_result ctxt #> not is_open ? Thm.close_derivation; fun after_qed res goal_ctxt = Proof_Context.put_thms false (Auto_Bind.thisN, diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/Pure.thy Sun Feb 16 17:50:13 2014 +0100 @@ -101,6 +101,7 @@ "ProofGeneral.inform_file_retracted" :: control begin +ML_file "ML/ml_thms.ML" ML_file "Isar/isar_syn.ML" ML_file "Isar/calculation.ML" ML_file "Tools/rail.ML" diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/ROOT --- a/src/Pure/ROOT Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/ROOT Sun Feb 16 17:50:13 2014 +0100 @@ -151,7 +151,6 @@ "ML/ml_statistics_dummy.ML" "ML/ml_statistics_polyml-5.5.0.ML" "ML/ml_syntax.ML" - "ML/ml_thms.ML" "PIDE/active.ML" "PIDE/command.ML" "PIDE/document.ML" diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/ROOT.ML Sun Feb 16 17:50:13 2014 +0100 @@ -260,7 +260,6 @@ use "Isar/spec_rules.ML"; use "Isar/specification.ML"; use "Isar/typedecl.ML"; -use "ML/ml_thms.ML"; (*toplevel transactions*) use "Isar/proof_node.ML"; diff -r bd67ebe275e0 -r a3870c12f254 src/Pure/build-jars --- a/src/Pure/build-jars Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Pure/build-jars Sun Feb 16 17:50:13 2014 +0100 @@ -13,6 +13,7 @@ Concurrent/future.scala Concurrent/simple_thread.scala Concurrent/volatile.scala + General/antiquote.scala General/bytes.scala General/exn.scala General/file.scala diff -r bd67ebe275e0 -r a3870c12f254 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Feb 16 17:50:13 2014 +0100 @@ -148,9 +148,15 @@ { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { - Swing_Thread.now { Document_Model(buffer) } match { - case Some(model) if model.is_theory => - val snapshot = model.snapshot + val opt_snapshot = + Swing_Thread.now { + Document_Model(buffer) match { + case Some(model) if model.is_theory => Some(model.snapshot) + case _ => None + } + } + opt_snapshot match { + case Some(snapshot) => val root = data.root for ((command, command_start) <- snapshot.node.command_range() if !stopped) { Isabelle_Sidekick.swing_markup_tree( @@ -172,7 +178,7 @@ }) } true - case _ => false + case None => false } } } diff -r bd67ebe275e0 -r a3870c12f254 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sun Feb 16 17:50:13 2014 +0100 @@ -129,6 +129,13 @@ ML_Lex.Kind.STRING -> LITERAL1, ML_Lex.Kind.SPACE -> NULL, ML_Lex.Kind.COMMENT -> COMMENT1, + ML_Lex.Kind.ANTIQ -> NULL, + ML_Lex.Kind.ANTIQ_START -> LITERAL4, + ML_Lex.Kind.ANTIQ_STOP -> LITERAL4, + ML_Lex.Kind.ANTIQ_OTHER -> NULL, + ML_Lex.Kind.ANTIQ_STRING -> NULL, + ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL, + ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL, ML_Lex.Kind.ERROR -> INVALID ).withDefaultValue(NULL) } @@ -599,7 +606,7 @@ private val foreground_include = - Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.ANTIQ) + Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQ) def foreground(range: Text.Range): List[Text.Info[Color]] = snapshot.select_markup(range, Some(foreground_include), _ => @@ -617,6 +624,7 @@ Markup.STRING -> Color.BLACK, Markup.ALTSTRING -> Color.BLACK, Markup.VERBATIM -> Color.BLACK, + Markup.CARTOUCHE -> Color.BLACK, Markup.LITERAL -> keyword1_color, Markup.DELIMITER -> Color.BLACK, Markup.TFREE -> tfree_color, diff -r bd67ebe275e0 -r a3870c12f254 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Sun Feb 16 13:56:48 2014 +0100 +++ b/src/Tools/jEdit/src/token_markup.scala Sun Feb 16 17:50:13 2014 +0100 @@ -177,7 +177,7 @@ private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN") - private class Line_Context(val context: Option[Scan.Context]) + private class Line_Context(val context: Option[Scan.Line_Context]) extends TokenMarker.LineContext(isabelle_rules, null) { override def hashCode: Int = context.hashCode @@ -204,14 +204,14 @@ { val (styled_tokens, context1) = if (mode == "isabelle-ml") { - val (tokens, ctxt1) = ML_Lex.tokenize_context(line, line_ctxt.get) + val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get) val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source)) (styled_tokens, new Line_Context(Some(ctxt1))) } else { Isabelle.mode_syntax(mode) match { case Some(syntax) if syntax.has_tokens && line_ctxt.isDefined => - val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get) + val (tokens, ctxt1) = syntax.scan_line(line, line_ctxt.get) val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) (styled_tokens, new Line_Context(Some(ctxt1)))