# HG changeset patch # User wenzelm # Date 1413621139 -7200 # Node ID 5bc1d6c4a499d4d810bf9d735cdf55a285d0493f # Parent 6b7445774ce3e8c919aea4f76f460f8e6410ab24 tuned signature; diff -r 6b7445774ce3 -r 5bc1d6c4a499 src/Pure/Isar/outer_syntax.scala --- 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)) } diff -r 6b7445774ce3 -r 5bc1d6c4a499 src/Tools/jEdit/src/bibtex_jedit.scala --- 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 */ diff -r 6b7445774ce3 -r 5bc1d6c4a499 src/Tools/jEdit/src/fold_handling.scala --- 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 } diff -r 6b7445774ce3 -r 5bc1d6c4a499 src/Tools/jEdit/src/token_markup.scala --- 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)