src/Pure/Isar/outer_syntax.scala
changeset 63603 9d9ea2c6bc38
parent 63592 64db21931bcb
child 63604 d8de4f8b95eb
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Aug 03 11:45:09 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Aug 04 10:55:51 2016 +0200
     1.3 @@ -44,22 +44,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* line-oriented structure */
     1.8 -
     1.9 -  object Line_Structure
    1.10 -  {
    1.11 -    val init = Line_Structure()
    1.12 -  }
    1.13 -
    1.14 -  sealed case class Line_Structure(
    1.15 -    improper: Boolean = true,
    1.16 -    command: Boolean = false,
    1.17 -    depth: Int = 0,
    1.18 -    span_depth: Int = 0,
    1.19 -    after_span_depth: Int = 0,
    1.20 -    element_depth: Int = 0)
    1.21 -
    1.22 -
    1.23    /* overall document structure */
    1.24  
    1.25    sealed abstract class Document { def length: Int }
    1.26 @@ -155,59 +139,6 @@
    1.27  
    1.28    /** parsing **/
    1.29  
    1.30 -  /* line-oriented structure */
    1.31 -
    1.32 -  private val close_structure =
    1.33 -    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END)
    1.34 -
    1.35 -  def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
    1.36 -    : Outer_Syntax.Line_Structure =
    1.37 -  {
    1.38 -    val improper1 = tokens.forall(_.is_improper)
    1.39 -    val command1 = tokens.exists(_.is_begin_or_command)
    1.40 -
    1.41 -    val command_depth =
    1.42 -      tokens.iterator.filter(_.is_proper).toStream.headOption match {
    1.43 -        case Some(tok) =>
    1.44 -          if (keywords.is_command(tok, close_structure))
    1.45 -            Some(structure.after_span_depth - 1)
    1.46 -          else None
    1.47 -        case None => None
    1.48 -      }
    1.49 -
    1.50 -    val depth0 = structure.element_depth
    1.51 -    val depth1 =
    1.52 -      if (tokens.exists(tok =>
    1.53 -            keywords.is_before_command(tok) ||
    1.54 -            !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0
    1.55 -      else if (command_depth.isDefined) command_depth.get
    1.56 -      else if (command1) structure.after_span_depth
    1.57 -      else structure.span_depth
    1.58 -
    1.59 -    val (span_depth1, after_span_depth1, element_depth1) =
    1.60 -      ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) {
    1.61 -        case (depths @ (x, y, z), tok) =>
    1.62 -          if (tok.is_begin) (z + 2, z + 1, z + 1)
    1.63 -          else if (tok.is_end) (z + 1, z - 1, z - 1)
    1.64 -          else if (tok.is_command) {
    1.65 -            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
    1.66 -            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
    1.67 -            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
    1.68 -            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
    1.69 -            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
    1.70 -            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
    1.71 -            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
    1.72 -            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
    1.73 -            else depths
    1.74 -          }
    1.75 -          else depths
    1.76 -      }
    1.77 -
    1.78 -    Outer_Syntax.Line_Structure(
    1.79 -      improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    1.80 -  }
    1.81 -
    1.82 -
    1.83    /* command spans */
    1.84  
    1.85    def parse_spans(toks: List[Token]): List[Command_Span.Span] =