src/Pure/Isar/outer_syntax.scala
changeset 58697 5bc1d6c4a499
parent 58696 6b7445774ce3
child 58700 4717d18cc619
     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