tuned signature;
authorwenzelm
Sat Oct 18 10:32:19 2014 +0200 (2014-10-18)
changeset 586975bc1d6c4a499
parent 58696 6b7445774ce3
child 58698 1be9855fb579
tuned signature;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/fold_handling.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 21:24:42 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 10:32:19 2014 +0200
     1.3 @@ -39,14 +39,14 @@
     1.4    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     1.5  
     1.6  
     1.7 -  /* line nesting */
     1.8 +  /* line-oriented structure */
     1.9  
    1.10 -  object Line_Nesting
    1.11 +  object Line_Structure
    1.12    {
    1.13 -    val init = Line_Nesting(0, 0)
    1.14 +    val init = Line_Structure(0, 0)
    1.15    }
    1.16  
    1.17 -  sealed case class Line_Nesting(depth_before: Int, depth: Int)
    1.18 +  sealed case class Line_Structure(depth_before: Int, depth: Int)
    1.19  }
    1.20  
    1.21  final class Outer_Syntax private(
    1.22 @@ -148,9 +148,9 @@
    1.23      heading_level(command.name)
    1.24  
    1.25  
    1.26 -  /* line nesting */
    1.27 +  /* line-oriented structure */
    1.28  
    1.29 -  def line_nesting(tokens: List[Token], depth: Int): Outer_Syntax.Line_Nesting =
    1.30 +  def line_structure(tokens: List[Token], depth: Int): Outer_Syntax.Line_Structure =
    1.31    {
    1.32      val depth1 =
    1.33        if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
    1.34 @@ -164,7 +164,7 @@
    1.35          else if (command_kind(tok, Keyword.qed_global)) 0
    1.36          else d
    1.37        }
    1.38 -    Outer_Syntax.Line_Nesting(depth1, depth2)
    1.39 +    Outer_Syntax.Line_Structure(depth1, depth2)
    1.40    }
    1.41  
    1.42  
    1.43 @@ -180,8 +180,11 @@
    1.44      }
    1.45    }
    1.46  
    1.47 -  def scan_line(input: CharSequence, context: Scan.Line_Context, nesting: Outer_Syntax.Line_Nesting)
    1.48 -    : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Nesting) =
    1.49 +  def scan_line(
    1.50 +    input: CharSequence,
    1.51 +    context: Scan.Line_Context,
    1.52 +    structure: Outer_Syntax.Line_Structure)
    1.53 +    : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) =
    1.54    {
    1.55      var in: Reader[Char] = new CharSequenceReader(input)
    1.56      val toks = new mutable.ListBuffer[Token]
    1.57 @@ -194,7 +197,7 @@
    1.58        }
    1.59      }
    1.60      val tokens = toks.toList
    1.61 -    (tokens, ctxt, line_nesting(tokens, nesting.depth))
    1.62 +    (tokens, ctxt, line_structure(tokens, structure.depth))
    1.63    }
    1.64  
    1.65  
     2.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Thu Oct 16 21:24:42 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sat Oct 18 10:32:19 2014 +0200
     2.3 @@ -155,7 +155,7 @@
     2.4  
     2.5    private class Line_Context(context: Option[Bibtex.Line_Context])
     2.6      extends Token_Markup.Generic_Line_Context[Bibtex.Line_Context](
     2.7 -      context_rules, context, Outer_Syntax.Line_Nesting.init)
     2.8 +      context_rules, context, Outer_Syntax.Line_Structure.init)
     2.9  
    2.10  
    2.11    /* token marker */
     3.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 21:24:42 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Sat Oct 18 10:32:19 2014 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4        }
     3.5  
     3.6      override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
     3.7 -      Token_Markup.buffer_line_nesting(buffer, line).depth_before
     3.8 +      Token_Markup.buffer_line_structure(buffer, line).depth_before
     3.9    }
    3.10  
    3.11  
     4.1 --- a/src/Tools/jEdit/src/token_markup.scala	Thu Oct 16 21:24:42 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Oct 18 10:32:19 2014 +0200
     4.3 @@ -178,14 +178,14 @@
     4.4    class Generic_Line_Context[C](
     4.5        rules: ParserRuleSet,
     4.6        val context: Option[C],
     4.7 -      val nesting: Outer_Syntax.Line_Nesting)
     4.8 +      val structure: Outer_Syntax.Line_Structure)
     4.9      extends TokenMarker.LineContext(rules, null)
    4.10    {
    4.11 -    override def hashCode: Int = (context, nesting).hashCode
    4.12 +    override def hashCode: Int = (context, structure).hashCode
    4.13      override def equals(that: Any): Boolean =
    4.14        that match {
    4.15          case other: Generic_Line_Context[_] =>
    4.16 -          context == other.context && nesting == other.nesting
    4.17 +          context == other.context && structure == other.structure
    4.18          case _ => false
    4.19        }
    4.20    }
    4.21 @@ -200,10 +200,10 @@
    4.22        case _ => None
    4.23      }
    4.24  
    4.25 -  def buffer_line_nesting(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Nesting =
    4.26 +  def buffer_line_structure(buffer: JEditBuffer, line: Int): Outer_Syntax.Line_Structure =
    4.27      buffer_line_context(buffer, line) match {
    4.28 -      case Some(c) => c.nesting
    4.29 -      case None => Outer_Syntax.Line_Nesting.init
    4.30 +      case Some(c) => c.structure
    4.31 +      case None => Outer_Syntax.Line_Structure.init
    4.32      }
    4.33  
    4.34  
    4.35 @@ -211,18 +211,20 @@
    4.36  
    4.37    private val context_rules = new ParserRuleSet("isabelle", "MAIN")
    4.38  
    4.39 -  private class Line_Context(context: Option[Scan.Line_Context], nesting: Outer_Syntax.Line_Nesting)
    4.40 -    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, nesting)
    4.41 +  private class Line_Context(
    4.42 +      context: Option[Scan.Line_Context],
    4.43 +      structure: Outer_Syntax.Line_Structure)
    4.44 +    extends Generic_Line_Context[Scan.Line_Context](context_rules, context, structure)
    4.45  
    4.46    class Marker(mode: String) extends TokenMarker
    4.47    {
    4.48      override def markTokens(context: TokenMarker.LineContext,
    4.49          handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
    4.50      {
    4.51 -      val (opt_ctxt, nesting) =
    4.52 +      val (opt_ctxt, structure) =
    4.53          context match {
    4.54 -          case c: Line_Context => (c.context, c.nesting)
    4.55 -          case _ => (Some(Scan.Finished), Outer_Syntax.Line_Nesting.init)
    4.56 +          case c: Line_Context => (c.context, c.structure)
    4.57 +          case _ => (Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
    4.58          }
    4.59        val line = if (raw_line == null) new Segment else raw_line
    4.60  
    4.61 @@ -233,17 +235,17 @@
    4.62              case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
    4.63                val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
    4.64                val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
    4.65 -              (styled_tokens, new Line_Context(Some(ctxt1), nesting))
    4.66 +              (styled_tokens, new Line_Context(Some(ctxt1), structure))
    4.67  
    4.68              case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
    4.69 -              val (tokens, ctxt1, nesting1) = syntax.scan_line(line, ctxt, nesting)
    4.70 +              val (tokens, ctxt1, structure1) = syntax.scan_line(line, ctxt, structure)
    4.71                val styled_tokens =
    4.72                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
    4.73 -              (styled_tokens, new Line_Context(Some(ctxt1), nesting1))
    4.74 +              (styled_tokens, new Line_Context(Some(ctxt1), structure1))
    4.75  
    4.76              case _ =>
    4.77                val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
    4.78 -              (List(styled_token), new Line_Context(None, nesting))
    4.79 +              (List(styled_token), new Line_Context(None, structure))
    4.80            }
    4.81  
    4.82          val extended = extended_styles(line)