--- a/src/Pure/Isar/outer_syntax.scala Wed Aug 03 11:45:09 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Aug 04 10:55:51 2016 +0200
@@ -44,22 +44,6 @@
}
- /* line-oriented structure */
-
- object Line_Structure
- {
- val init = Line_Structure()
- }
-
- sealed case class Line_Structure(
- improper: Boolean = true,
- command: Boolean = false,
- depth: Int = 0,
- span_depth: Int = 0,
- after_span_depth: Int = 0,
- element_depth: Int = 0)
-
-
/* overall document structure */
sealed abstract class Document { def length: Int }
@@ -155,59 +139,6 @@
/** parsing **/
- /* line-oriented structure */
-
- private val close_structure =
- Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END)
-
- def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
- : Outer_Syntax.Line_Structure =
- {
- val improper1 = tokens.forall(_.is_improper)
- val command1 = tokens.exists(_.is_begin_or_command)
-
- val command_depth =
- tokens.iterator.filter(_.is_proper).toStream.headOption match {
- case Some(tok) =>
- if (keywords.is_command(tok, close_structure))
- Some(structure.after_span_depth - 1)
- else None
- case None => None
- }
-
- val depth0 = structure.element_depth
- val depth1 =
- if (tokens.exists(tok =>
- keywords.is_before_command(tok) ||
- !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0
- else if (command_depth.isDefined) command_depth.get
- else if (command1) structure.after_span_depth
- else structure.span_depth
-
- val (span_depth1, after_span_depth1, element_depth1) =
- ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) {
- case (depths @ (x, y, z), tok) =>
- if (tok.is_begin) (z + 2, z + 1, z + 1)
- else if (tok.is_end) (z + 1, z - 1, z - 1)
- else if (tok.is_command) {
- if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
- else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
- else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
- else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
- else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
- else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
- else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
- else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
- else depths
- }
- else depths
- }
-
- Outer_Syntax.Line_Structure(
- improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
- }
-
-
/* command spans */
def parse_spans(toks: List[Token]): List[Command_Span.Span] =