--- 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 **/
--- /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)
+ }
+}
--- 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] =
--- 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
--- 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))