# HG changeset patch # User wenzelm # Date 1470300951 -7200 # Node ID 9d9ea2c6bc38989ed37c67554423c5008733e28d # Parent 64db21931bcbfadc84b0343d2b08dae5ac26db8e clarified modules; diff -r 64db21931bcb -r 9d9ea2c6bc38 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Wed Aug 03 11:45:09 2016 +0200 +++ b/src/Pure/Isar/keyword.scala Thu Aug 04 10:55:51 2016 +0200 @@ -87,6 +87,8 @@ val proof_close = qed + PRF_CLOSE val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE) + val close_structure = Set(NEXT_BLOCK, QED_BLOCK, PRF_CLOSE, THY_END) + /** keyword tables **/ diff -r 64db21931bcb -r 9d9ea2c6bc38 src/Pure/Isar/line_structure.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/line_structure.scala Thu Aug 04 10:55:51 2016 +0200 @@ -0,0 +1,67 @@ +/* Title: Pure/Isar/line_structure.scala + Author: Makarius + +Line-oriented document structure, e.g. for fold handling. +*/ + +package isabelle + + +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) +{ + def update(keywords: Keyword.Keywords, tokens: List[Token]): 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, Keyword.close_structure)) + Some(after_span_depth - 1) + else None + case None => None + } + + val depth1 = + if (tokens.exists(tok => + keywords.is_before_command(tok) || + !tok.is_end && keywords.is_command(tok, Keyword.theory))) element_depth + else if (command_depth.isDefined) command_depth.get + else if (command1) after_span_depth + else span_depth + + val (span_depth1, after_span_depth1, element_depth1) = + ((span_depth, after_span_depth, 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) { + val depth0 = element_depth + 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 + } + + Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1) + } +} diff -r 64db21931bcb -r 9d9ea2c6bc38 src/Pure/Isar/outer_syntax.scala --- 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] = diff -r 64db21931bcb -r 9d9ea2c6bc38 src/Pure/build-jars --- a/src/Pure/build-jars Wed Aug 03 11:45:09 2016 +0200 +++ b/src/Pure/build-jars Thu Aug 04 10:55:51 2016 +0200 @@ -50,6 +50,7 @@ General/word.scala General/xz_file.scala Isar/keyword.scala + Isar/line_structure.scala Isar/outer_syntax.scala Isar/parse.scala Isar/token.scala diff -r 64db21931bcb -r 9d9ea2c6bc38 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Wed Aug 03 11:45:09 2016 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Thu Aug 04 10:55:51 2016 +0200 @@ -178,7 +178,7 @@ object Line_Context { def init(mode: String): Line_Context = - new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init) + new Line_Context(mode, Some(Scan.Finished), Line_Structure.init) def prev(buffer: JEditBuffer, line: Int): Line_Context = if (line == 0) init(JEdit_Lib.buffer_mode(buffer)) @@ -202,7 +202,7 @@ class Line_Context( val mode: String, val context: Option[Scan.Line_Context], - val structure: Outer_Syntax.Line_Structure) + val structure: Line_Structure) extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null) { def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished) @@ -406,7 +406,7 @@ case (Some(ctxt), Some(syntax)) if syntax.has_tokens => val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt) - val structure1 = syntax.line_structure(tokens, structure) + val structure1 = structure.update(syntax.keywords, tokens) val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source)) (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))