src/Pure/Isar/outer_syntax.scala
changeset 59924 801b979ec0c2
parent 59735 24bee1b11fce
child 59939 7d46aa03696e
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Apr 04 14:04:11 2015 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Apr 04 21:21:40 2015 +0200
     1.3 @@ -149,7 +149,7 @@
     1.4  
     1.5    /* line-oriented structure */
     1.6  
     1.7 -  def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
     1.8 +  def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
     1.9      : Outer_Syntax.Line_Structure =
    1.10    {
    1.11      val improper1 = tokens.forall(_.is_improper)
    1.12 @@ -157,11 +157,11 @@
    1.13  
    1.14      val depth1 =
    1.15        if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
    1.16 -      else if (command1) struct.after_span_depth
    1.17 -      else struct.span_depth
    1.18 +      else if (command1) structure.after_span_depth
    1.19 +      else structure.span_depth
    1.20  
    1.21      val (span_depth1, after_span_depth1) =
    1.22 -      ((struct.span_depth, struct.after_span_depth) /: tokens) {
    1.23 +      ((structure.span_depth, structure.after_span_depth) /: tokens) {
    1.24          case ((x, y), tok) =>
    1.25            if (tok.is_command) {
    1.26              if (tok.is_command_kind(keywords, Keyword.theory_goal))
    1.27 @@ -194,13 +194,20 @@
    1.28      def ship(span: List[Token])
    1.29      {
    1.30        val kind =
    1.31 -        if (span.nonEmpty && span.head.is_command && !span.exists(_.is_error)) {
    1.32 -          val name = span.head.source
    1.33 -          val pos = Position.Range(Text.Range(0, Symbol.iterator(name).length) + 1)
    1.34 -          Command_Span.Command_Span(name, pos)
    1.35 -        }
    1.36 -        else if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    1.37 -        else Command_Span.Malformed_Span
    1.38 +        if (span.forall(_.is_improper)) Command_Span.Ignored_Span
    1.39 +        else if (span.exists(_.is_error)) Command_Span.Malformed_Span
    1.40 +        else
    1.41 +          span.find(_.is_command) match {
    1.42 +            case None => Command_Span.Malformed_Span
    1.43 +            case Some(cmd) =>
    1.44 +              val name = cmd.source
    1.45 +              val offset =
    1.46 +                (0 /: span.takeWhile(_ != cmd)) {
    1.47 +                  case (i, tok) => i + Symbol.iterator(tok.source).length }
    1.48 +              val end_offset = offset + Symbol.iterator(name).length
    1.49 +              val pos = Position.Range(Text.Range(offset, end_offset) + 1)
    1.50 +              Command_Span.Command_Span(name, pos)
    1.51 +          }
    1.52        result += Command_Span.Span(kind, span)
    1.53      }
    1.54  
    1.55 @@ -211,8 +218,10 @@
    1.56      }
    1.57  
    1.58      for (tok <- toks) {
    1.59 -      if (tok.is_command) { flush(); content += tok }
    1.60 -      else if (tok.is_improper) improper += tok
    1.61 +      if (tok.is_improper) improper += tok
    1.62 +      else if (tok.is_private ||
    1.63 +        tok.is_command && (!content.exists(_.is_private) || content.exists(_.is_command)))
    1.64 +      { flush(); content += tok }
    1.65        else { content ++= improper; improper.clear; content += tok }
    1.66      }
    1.67      flush()