--- a/src/Pure/Isar/outer_syntax.scala Thu Oct 16 21:24:42 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sat Oct 18 10:32:19 2014 +0200
@@ -39,14 +39,14 @@
def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
- /* line nesting */
+ /* line-oriented structure */
- object Line_Nesting
+ object Line_Structure
{
- val init = Line_Nesting(0, 0)
+ val init = Line_Structure(0, 0)
}
- sealed case class Line_Nesting(depth_before: Int, depth: Int)
+ sealed case class Line_Structure(depth_before: Int, depth: Int)
}
final class Outer_Syntax private(
@@ -148,9 +148,9 @@
heading_level(command.name)
- /* line nesting */
+ /* line-oriented structure */
- def line_nesting(tokens: List[Token], depth: Int): Outer_Syntax.Line_Nesting =
+ def line_structure(tokens: List[Token], depth: Int): Outer_Syntax.Line_Structure =
{
val depth1 =
if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
@@ -164,7 +164,7 @@
else if (command_kind(tok, Keyword.qed_global)) 0
else d
}
- Outer_Syntax.Line_Nesting(depth1, depth2)
+ Outer_Syntax.Line_Structure(depth1, depth2)
}
@@ -180,8 +180,11 @@
}
}
- def scan_line(input: CharSequence, context: Scan.Line_Context, nesting: Outer_Syntax.Line_Nesting)
- : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Nesting) =
+ def scan_line(
+ input: CharSequence,
+ context: Scan.Line_Context,
+ structure: Outer_Syntax.Line_Structure)
+ : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) =
{
var in: Reader[Char] = new CharSequenceReader(input)
val toks = new mutable.ListBuffer[Token]
@@ -194,7 +197,7 @@
}
}
val tokens = toks.toList
- (tokens, ctxt, line_nesting(tokens, nesting.depth))
+ (tokens, ctxt, line_structure(tokens, structure.depth))
}
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Thu Oct 16 21:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sat Oct 18 10:32:19 2014 +0200
@@ -155,7 +155,7 @@
private class Line_Context(context: Option[Bibtex.Line_Context])
extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](
- context_rules, context, Outer_Syntax.Line_Nesting.init)
+ context_rules, context, Outer_Syntax.Line_Structure.init)
/* token marker */
--- a/src/Tools/jEdit/src/fold_handling.scala Thu Oct 16 21:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala Sat Oct 18 10:32:19 2014 +0200
@@ -27,7 +27,7 @@
}
override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
- Token_Markup.buffer_line_nesting(buffer, line).depth_before
+ Token_Markup.buffer_line_structure(buffer, line).depth_before
}
--- a/src/Tools/jEdit/src/token_markup.scala Thu Oct 16 21:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Sat Oct 18 10:32:19 2014 +0200
@@ -178,14 +178,14 @@
class Generic_Line_Context[C](
rules: ParserRuleSet,
val context: Option[C],
- val nesting: Outer_Syntax.Line_Nesting)
+ val structure: Outer_Syntax.Line_Structure)
extends TokenMarker.LineContext(rules, null)
{
- override def hashCode: Int = (context, nesting).hashCode
+ override def hashCode: Int = (context, structure).hashCode
override def equals(that: Any): Boolean =
that match {
case other: Generic_Line_Context[_] =>
- context == other.context && nesting == other.nesting
+ context == other.context && structure == other.structure
case _ => false
}
}
@@ -200,10 +200,10 @@
case _ => None
}
- def buffer_line_nesting(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Nesting =
+ def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
buffer_line_context(buffer, line) match {
- case Some(c) => c.nesting
- case None => Outer_Syntax.Line_Nesting.init
+ case Some(c) => c.structure
+ case None => Outer_Syntax.Line_Structure.init
}
@@ -211,18 +211,20 @@
private val context_rules = new ParserRuleSet("isabelle", "MAIN")
- private class Line_Context(context: Option[Scan.Line_Context], nesting: Outer_Syntax.Line_Nesting)
- extends Generic_Line_Context[Scan.Line_Context](context_rules, context, nesting)
+ private class Line_Context(
+ context: Option[Scan.Line_Context],
+ structure: Outer_Syntax.Line_Structure)
+ extends Generic_Line_Context[Scan.Line_Context](context_rules, context, structure)
class Marker(mode: String) extends TokenMarker
{
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
{
- val (opt_ctxt, nesting) =
+ val (opt_ctxt, structure) =
context match {
- case c: Line_Context => (c.context, c.nesting)
- case _ => (Some(Scan.Finished), Outer_Syntax.Line_Nesting.init)
+ case c: Line_Context => (c.context, c.structure)
+ case _ => (Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
}
val line = if (raw_line == null) new Segment else raw_line
@@ -233,17 +235,17 @@
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), nesting))
+ (styled_tokens, new Line_Context(Some(ctxt1), structure))
case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
- val (tokens, ctxt1, nesting1) = syntax.scan_line(line, ctxt, nesting)
+ val (tokens, ctxt1, structure1) = syntax.scan_line(line, ctxt, structure)
val styled_tokens =
tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
- (styled_tokens, new Line_Context(Some(ctxt1), nesting1))
+ (styled_tokens, new Line_Context(Some(ctxt1), structure1))
case _ =>
val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
- (List(styled_token), new Line_Context(None, nesting))
+ (List(styled_token), new Line_Context(None, structure))
}
val extended = extended_styles(line)