--- a/NEWS Mon Jul 11 21:02:26 2016 +0200
+++ b/NEWS Mon Jul 11 22:07:02 2016 +0200
@@ -76,6 +76,9 @@
* Highlighting of entity def/ref positions wrt. cursor.
+* Indentation according to Isabelle outer syntax, cf. action
+"indent-lines" (shortcut C+i).
+
* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
occurences of the formal entity at the caret position. This facilitates
systematic renaming.
--- a/src/Pure/General/word.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/General/word.scala Mon Jul 11 22:07:02 2016 +0200
@@ -96,4 +96,10 @@
def explode(text: String): List[String] =
explode(Character.isWhitespace(_), text)
+
+
+ /* brackets */
+
+ val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
+ val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
}
--- a/src/Pure/Isar/keyword.ML Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Jul 11 22:07:02 2016 +0200
@@ -32,9 +32,11 @@
val prf_script: string
val prf_script_goal: string
val prf_script_asm_goal: string
+ val before_command: string
val quasi_command: string
type spec = (string * string list) * string list
val no_spec: spec
+ val before_command_spec: spec
val quasi_command_spec: spec
type keywords
val minor_keywords: keywords -> Scan.lexicon
@@ -107,6 +109,8 @@
val prf_script = "prf_script";
val prf_script_goal = "prf_script_goal";
val prf_script_asm_goal = "prf_script_asm_goal";
+
+val before_command = "before_command";
val quasi_command = "quasi_command";
val command_kinds =
@@ -121,6 +125,7 @@
type spec = (string * string list) * string list;
val no_spec: spec = (("", []), []);
+val before_command_spec: spec = ((before_command, []), []);
val quasi_command_spec: spec = ((quasi_command, []), []);
type entry =
@@ -175,7 +180,7 @@
val add_keywords =
fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
- if kind = "" orelse kind = quasi_command then
+ if kind = "" orelse kind = before_command orelse kind = quasi_command then
let
val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
in (minor', major, commands) end
--- a/src/Pure/Isar/keyword.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/keyword.scala Mon Jul 11 22:07:02 2016 +0200
@@ -39,6 +39,8 @@
val PRF_SCRIPT = "prf_script"
val PRF_SCRIPT_GOAL = "prf_script_goal"
val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
+
+ val BEFORE_COMMAND = "before_command"
val QUASI_COMMAND = "quasi_command"
@@ -90,6 +92,7 @@
type Spec = ((String, List[String]), List[String])
val no_spec: Spec = (("", Nil), Nil)
+ val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
object Keywords
@@ -100,22 +103,20 @@
class Keywords private(
val minor: Scan.Lexicon = Scan.Lexicon.empty,
val major: Scan.Lexicon = Scan.Lexicon.empty,
- protected val quasi_commands: Set[String] = Set.empty,
- protected val commands: Map[String, (String, List[String])] = Map.empty)
+ val kinds: Map[String, String] = Map.empty,
+ val load_commands: Map[String, List[String]] = Map.empty)
{
override def toString: String =
{
- val keywords1 =
- for (name <- minor.iterator.toList) yield {
- if (quasi_commands.contains(name)) (name, quote(name) + " :: \"quasi_command\"")
- else (name, quote(name))
+ val entries =
+ for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
+ val exts = load_commands.getOrElse(name, Nil)
+ val kind_decl =
+ if (kind == "") ""
+ else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
+ quote(name) + kind_decl
}
- val keywords2 =
- for ((name, (kind, files)) <- commands.toList) yield {
- (name, quote(name) + " :: " + quote(kind) +
- (if (files.isEmpty) "" else " (" + commas_quote(files) + ")"))
- }
- (keywords1 ::: keywords2).sortBy(_._1).map(_._2).mkString("keywords\n ", " and\n ", "")
+ entries.mkString("keywords\n ", " and\n ", "")
}
@@ -129,58 +130,58 @@
else {
val minor1 = minor ++ other.minor
val major1 = major ++ other.major
- val quasi_commands1 = quasi_commands ++ other.quasi_commands
- val commands1 =
- if (commands eq other.commands) commands
- else if (commands.isEmpty) other.commands
- else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
- new Keywords(minor1, major1, quasi_commands1, commands1)
+ val kinds1 =
+ if (kinds eq other.kinds) kinds
+ else if (kinds.isEmpty) other.kinds
+ else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ val load_commands1 =
+ if (load_commands eq other.load_commands) load_commands
+ else if (load_commands.isEmpty) other.load_commands
+ else
+ (load_commands /: other.load_commands) {
+ case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ new Keywords(minor1, major1, kinds1, load_commands1)
}
/* add keywords */
- def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
- if (kind == "") new Keywords(minor + name, major, quasi_commands, commands)
- else if (kind == QUASI_COMMAND)
- new Keywords(minor + name, major, quasi_commands + name, commands)
- else {
- val major1 = major + name
- val commands1 = commands + (name -> (kind, tags))
- new Keywords(minor, major1, quasi_commands, commands1)
- }
+ def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
+ {
+ val kinds1 = kinds + (name -> kind)
+ val (minor1, major1) =
+ if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND)
+ (minor + name, major)
+ else (minor, major + name)
+ val load_commands1 =
+ if (kind == THY_LOAD) load_commands + (name -> exts)
+ else load_commands
+ new Keywords(minor1, major1, kinds1, load_commands1)
+ }
def add_keywords(header: Thy_Header.Keywords): Keywords =
(this /: header) {
- case (keywords, (name, ((kind, tags), _), _)) =>
+ case (keywords, (name, ((kind, exts), _), _)) =>
if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
- else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+ else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
}
/* command kind */
- def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
-
def is_command(token: Token, check_kind: String => Boolean): Boolean =
token.is_command &&
- (command_kind(token.source) match { case Some(k) => check_kind(k) case None => false })
+ (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
+
+ def is_before_command(token: Token): Boolean =
+ token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
def is_quasi_command(token: Token): Boolean =
- token.is_keyword && quasi_commands.contains(token.source)
+ token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
/* load commands */
- def load_command(name: String): Option[List[String]] =
- commands.get(name) match {
- case Some((THY_LOAD, exts)) => Some(exts)
- case _ => None
- }
-
- private lazy val load_commands: List[(String, List[String])] =
- (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
-
def load_commands_in(text: String): Boolean =
load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
}
--- a/src/Pure/Isar/outer_syntax.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Mon Jul 11 22:07:02 2016 +0200
@@ -118,7 +118,7 @@
/* load commands */
- def load_command(name: String): Option[List[String]] = keywords.load_command(name)
+ def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
@@ -209,8 +209,9 @@
for (tok <- toks) {
if (tok.is_improper) improper += tok
- else if (tok.is_command_modifier ||
- tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
+ else if (keywords.is_before_command(tok) ||
+ tok.is_command &&
+ (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
{ flush(); content += tok }
else { content ++= improper; improper.clear; content += tok }
}
@@ -236,7 +237,7 @@
case Thy_Header.PARAGRAPH => Some(4)
case Thy_Header.SUBPARAGRAPH => Some(5)
case _ =>
- keywords.command_kind(name) match {
+ keywords.kinds.get(name) match {
case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
case _ => None
}
--- a/src/Pure/Isar/parse.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/parse.scala Mon Jul 11 22:07:02 2016 +0200
@@ -59,12 +59,8 @@
def atom(s: String, pred: Elem => Boolean): Parser[String] =
token(s, pred) ^^ (_.content)
- def command(name: String): Parser[String] =
- atom("command " + quote(name), tok => tok.is_command && tok.source == name)
-
- def $$$(name: String): Parser[String] =
- atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
-
+ def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name))
+ def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name))
def string: Parser[String] = atom("string", _.is_string)
def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
def name: Parser[String] = atom("name", _.is_name)
--- a/src/Pure/Isar/token.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/token.scala Mon Jul 11 22:07:02 2016 +0200
@@ -225,7 +225,11 @@
sealed case class Token(kind: Token.Kind.Value, source: String)
{
def is_command: Boolean = kind == Token.Kind.COMMAND
+ def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name
def is_keyword: Boolean = kind == Token.Kind.KEYWORD
+ def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name
+ def is_keyword(name: Char): Boolean =
+ kind == Token.Kind.KEYWORD && source.length == 1 && source(0) == name
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
def is_ident: Boolean = kind == Token.Kind.IDENT
def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
@@ -254,12 +258,11 @@
source.startsWith(Symbol.open) ||
source.startsWith(Symbol.open_decoded))
- def is_begin: Boolean = is_keyword && source == "begin"
- def is_end: Boolean = is_command && source == "end"
+ def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_))
+ def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_))
- // FIXME avoid hard-wired stuff
- def is_command_modifier: Boolean =
- is_keyword && (source == "public" || source == "private" || source == "qualified")
+ def is_begin: Boolean = is_keyword("begin")
+ def is_end: Boolean = is_command("end")
def content: String =
if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
--- a/src/Pure/Pure.thy Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Pure.thy Mon Jul 11 22:07:02 2016 +0200
@@ -8,10 +8,10 @@
keywords
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
- "open" "output" "overloaded" "pervasive" "premises" "private" "qualified"
- "structure" "unchecked" "where" "when" "|"
+ "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
+ and "private" "qualified" :: before_command
and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
- "obtains" "shows" :: quasi_command
+ "obtains" "shows" "where" "|" :: quasi_command
and "text" "txt" :: document_body
and "text_raw" :: document_raw
and "default_sort" :: thy_decl == ""
--- a/src/Pure/System/options.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/System/options.scala Mon Jul 11 22:07:02 2016 +0200
@@ -76,7 +76,9 @@
lazy val options_syntax =
Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
- (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL)
+ (SECTION, Keyword.DOCUMENT_HEADING) +
+ (PUBLIC, Keyword.BEFORE_COMMAND) +
+ (OPTION, Keyword.THY_DECL)
lazy val prefs_syntax = Outer_Syntax.init() + "="
--- a/src/Pure/Thy/sessions.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Jul 11 22:07:02 2016 +0200
@@ -163,9 +163,15 @@
private val DOCUMENT_FILES = "document_files"
lazy val root_syntax =
- Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
- (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
- IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
+ Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
+ (CHAPTER, Keyword.THY_DECL) +
+ (SESSION, Keyword.THY_DECL) +
+ (DESCRIPTION, Keyword.QUASI_COMMAND) +
+ (OPTIONS, Keyword.QUASI_COMMAND) +
+ (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
+ (THEORIES, Keyword.QUASI_COMMAND) +
+ (FILES, Keyword.QUASI_COMMAND) +
+ (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
private object Parser extends Parse.Parser with Options.Parser
{
--- a/src/Pure/Thy/thy_header.ML Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Jul 11 22:07:02 2016 +0200
@@ -70,9 +70,9 @@
(("::", @{here}), Keyword.no_spec),
(("==", @{here}), Keyword.no_spec),
(("and", @{here}), Keyword.no_spec),
- ((beginN, @{here}), Keyword.no_spec),
- ((importsN, @{here}), Keyword.no_spec),
- ((keywordsN, @{here}), Keyword.no_spec),
+ ((beginN, @{here}), Keyword.quasi_command_spec),
+ ((importsN, @{here}), Keyword.quasi_command_spec),
+ ((keywordsN, @{here}), Keyword.quasi_command_spec),
((chapterN, @{here}), ((Keyword.document_heading, []), [])),
((sectionN, @{here}), ((Keyword.document_heading, []), [])),
((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
--- a/src/Pure/Thy/thy_header.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Jul 11 22:07:02 2016 +0200
@@ -44,9 +44,9 @@
("::", Keyword.no_spec, None),
("==", Keyword.no_spec, None),
(AND, Keyword.no_spec, None),
- (BEGIN, Keyword.no_spec, None),
- (IMPORTS, Keyword.no_spec, None),
- (KEYWORDS, Keyword.no_spec, None),
+ (BEGIN, Keyword.quasi_command_spec, None),
+ (IMPORTS, Keyword.quasi_command_spec, None),
+ (KEYWORDS, Keyword.quasi_command_spec, None),
(CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
(SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
--- a/src/Tools/jEdit/src/document_model.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Jul 11 22:07:02 2016 +0200
@@ -96,8 +96,7 @@
Token_Markup.line_token_iterator(
Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
{
- case Text.Info(range, tok)
- if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+ case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start
})
match {
case Some(offset) =>
--- a/src/Tools/jEdit/src/isabelle.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Jul 11 22:07:02 2016 +0200
@@ -87,7 +87,11 @@
/* text structure */
def indent_rule(mode: String): Option[IndentRule] =
- if (mode == "isabelle") Some(Text_Structure.Indent_Rule) else None
+ mode match {
+ case "isabelle" | "isabelle-options" | "isabelle-root" =>
+ Some(Text_Structure.Indent_Rule)
+ case _ => None
+ }
def structure_matchers(mode: String): List[StructureMatcher] =
if (mode == "isabelle") List(Text_Structure.Matcher) else Nil
--- a/src/Tools/jEdit/src/rendering.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Mon Jul 11 22:07:02 2016 +0200
@@ -93,7 +93,7 @@
}
def token_markup(syntax: Outer_Syntax, token: Token): Byte =
- if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
+ if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL
else if (token.is_delimiter) JEditToken.OPERATOR
else token_style(token.kind)
--- a/src/Tools/jEdit/src/text_structure.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Mon Jul 11 22:07:02 2016 +0200
@@ -19,17 +19,21 @@
{
/* token navigator */
- class Navigator(syntax: Outer_Syntax, buffer: Buffer)
+ class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
{
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
- Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
- filter(_.info.is_proper)
+ {
+ val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
+ if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
+ }
def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
- Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
- filter(_.info.is_proper)
+ {
+ val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
+ if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
+ }
}
@@ -46,7 +50,7 @@
Isabelle.buffer_syntax(buffer) match {
case Some(syntax) if buffer.isInstanceOf[Buffer] =>
val keywords = syntax.keywords
- val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
+ val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
def head_token(line: Int): Option[Token] =
nav.iterator(line, 1).toStream.headOption.map(_.info)
@@ -64,6 +68,9 @@
def prev_span: Iterator[Token] =
nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command)
+ def prev_line_span: Iterator[Token] =
+ nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command)
+
def line_indent(line: Int): Int =
if (line < 0 || line >= buffer.getLineCount) 0
@@ -77,9 +84,16 @@
else 0
def indent_offset(tok: Token): Int =
- if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
+ if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size
else 0
+ def indent_brackets: Int =
+ (0 /: prev_line_span)(
+ { case (i, tok) =>
+ if (tok.is_open_bracket) i + indent_size
+ else if (tok.is_close_bracket) i - indent_size
+ else i })
+
def indent_extra: Int =
if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
else 0
@@ -97,12 +111,20 @@
else (ind1, false)
}).collectFirst({ case (i, true) => i }).getOrElse(0)
+ def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int =
+ (0 /: it)({ case (d, tok) => if (open(tok)) d + 1 else if (close(tok)) d - 1 else d })
+
+ def indent_begin: Int =
+ (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) *
+ indent_size
+
val indent =
head_token(current_line) match {
- case None => indent_structure + indent_extra
+ case None => indent_structure + indent_brackets + indent_extra
case Some(tok) =>
- if (keywords.is_command(tok, Keyword.theory)) 0
- else if (tok.is_command) indent_structure - indent_offset(tok)
+ if (keywords.is_before_command(tok) ||
+ keywords.is_command(tok, Keyword.theory)) indent_begin
+ else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
else {
prev_command match {
case None =>
@@ -112,16 +134,16 @@
case (true, false) => - indent_extra
case (false, true) => indent_extra
}
- line_indent(prev_line) + extra
+ line_indent(prev_line) - indent_offset(tok) + indent_brackets + extra
case Some(prev_tok) =>
- indent_structure - indent_offset(prev_tok) -
- indent_indent(prev_tok) + indent_size
+ indent_structure - indent_offset(tok) - indent_offset(prev_tok) +
+ indent_brackets - indent_indent(prev_tok) + indent_size
}
}
}
actions.clear()
- actions.add(new IndentAction.AlignOffset(indent))
+ actions.add(new IndentAction.AlignOffset(indent max 0))
case _ =>
}
}
@@ -160,7 +182,7 @@
case Some(syntax) if buffer.isInstanceOf[Buffer] =>
val keywords = syntax.keywords
- val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
+ val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
def caret_iterator(): Iterator[Text.Info[Token]] =
nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
--- a/src/Tools/jEdit/src/token_markup.scala Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Jul 11 22:07:02 2016 +0200
@@ -175,22 +175,23 @@
/* line context */
- private val context_rules = new ParserRuleSet("isabelle", "MAIN")
-
object Line_Context
{
- val init = new Line_Context(Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
+ def init(mode: String): Line_Context =
+ new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
}
class Line_Context(
+ val mode: String,
val context: Option[Scan.Line_Context],
val structure: Outer_Syntax.Line_Structure)
- extends TokenMarker.LineContext(context_rules, null)
+ extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
{
- override def hashCode: Int = (context, structure).hashCode
+ override def hashCode: Int = (mode, context, structure).hashCode
override def equals(that: Any): Boolean =
that match {
- case other: Line_Context => context == other.context && structure == other.structure
+ case other: Line_Context =>
+ mode == other.mode && context == other.context && structure == other.structure
case _ => false
}
}
@@ -205,7 +206,7 @@
}
context getOrElse {
buffer.markTokens(line, DummyTokenHandler.INSTANCE)
- context getOrElse Line_Context.init
+ context getOrElse Line_Context.init(JEdit_Lib.buffer_mode(buffer))
}
}
@@ -216,7 +217,7 @@
: Option[List[Token]] =
{
val line_context =
- if (line == 0) Line_Context.init
+ if (line == 0) Line_Context.init(JEdit_Lib.buffer_mode(buffer))
else buffer_line_context(buffer, line - 1)
for {
ctxt <- line_context.context
@@ -275,13 +276,15 @@
def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
: Option[Text.Info[Command_Span.Span]] =
{
+ val keywords = syntax.keywords
+
def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
token_reverse_iterator(syntax, buffer, i).
- find(info => info.info.is_command_modifier || info.info.is_command)
+ find(info => keywords.is_before_command(info.info) || info.info.is_command)
def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
token_iterator(syntax, buffer, i).
- find(info => info.info.is_command_modifier || info.info.is_command)
+ find(info => keywords.is_before_command(info.info) || info.info.is_command)
if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
val start_info =
@@ -291,15 +294,16 @@
case Some(Text.Info(range1, tok1)) if tok1.is_command =>
val info2 = maybe_command_start(range1.start - 1)
info2 match {
- case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
+ case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
case _ => info1
}
case _ => info1
}
}
- val (start_is_command_modifier, start, start_next) =
+ val (start_before_command, start, start_next) =
start_info match {
- case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
+ case Some(Text.Info(range, tok)) =>
+ (keywords.is_before_command(tok), range.start, range.stop)
case None => (false, 0, 0)
}
@@ -307,7 +311,7 @@
{
val info1 = maybe_command_stop(start_next)
info1 match {
- case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
+ case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
maybe_command_stop(range1.stop)
case _ => info1
}
@@ -378,7 +382,8 @@
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
{
val line = if (raw_line == null) new Segment else raw_line
- val line_context = context match { case c: Line_Context => c case _ => Line_Context.init }
+ val line_context =
+ context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
val structure = line_context.structure
val context1 =
@@ -393,18 +398,18 @@
case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
- (styled_tokens, new Line_Context(Some(ctxt1), structure))
+ (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
val structure1 = syntax.line_structure(tokens, structure)
val styled_tokens =
tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
- (styled_tokens, new Line_Context(Some(ctxt1), structure1))
+ (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
case _ =>
val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
- (List(styled_token), new Line_Context(None, structure))
+ (List(styled_token), new Line_Context(line_context.mode, None, structure))
}
val extended = extended_styles(line)