clarified modules;
authorwenzelm
Thu Aug 04 10:55:51 2016 +0200 (2016-08-04)
changeset 636039d9ea2c6bc38
parent 63592 64db21931bcb
child 63604 d8de4f8b95eb
clarified modules;
src/Pure/Isar/keyword.scala
src/Pure/Isar/line_structure.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/build-jars
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Wed Aug 03 11:45:09 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Thu Aug 04 10:55:51 2016 +0200
     1.3 @@ -87,6 +87,8 @@
     1.4    val proof_close = qed + PRF_CLOSE
     1.5    val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE)
     1.6  
     1.7 +  val close_structure = Set(NEXT_BLOCK, QED_BLOCK, PRF_CLOSE, THY_END)
     1.8 +
     1.9  
    1.10  
    1.11    /** keyword tables **/
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Isar/line_structure.scala	Thu Aug 04 10:55:51 2016 +0200
     2.3 @@ -0,0 +1,67 @@
     2.4 +/*  Title:      Pure/Isar/line_structure.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Line-oriented document structure, e.g. for fold handling.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Line_Structure
    2.14 +{
    2.15 +  val init = Line_Structure()
    2.16 +}
    2.17 +
    2.18 +sealed case class Line_Structure(
    2.19 +  improper: Boolean = true,
    2.20 +  command: Boolean = false,
    2.21 +  depth: Int = 0,
    2.22 +  span_depth: Int = 0,
    2.23 +  after_span_depth: Int = 0,
    2.24 +  element_depth: Int = 0)
    2.25 +{
    2.26 +  def update(keywords: Keyword.Keywords, tokens: List[Token]): Line_Structure =
    2.27 +  {
    2.28 +    val improper1 = tokens.forall(_.is_improper)
    2.29 +    val command1 = tokens.exists(_.is_begin_or_command)
    2.30 +
    2.31 +    val command_depth =
    2.32 +      tokens.iterator.filter(_.is_proper).toStream.headOption match {
    2.33 +        case Some(tok) =>
    2.34 +          if (keywords.is_command(tok, Keyword.close_structure))
    2.35 +            Some(after_span_depth - 1)
    2.36 +          else None
    2.37 +        case None => None
    2.38 +      }
    2.39 +
    2.40 +    val depth1 =
    2.41 +      if (tokens.exists(tok =>
    2.42 +            keywords.is_before_command(tok) ||
    2.43 +            !tok.is_end && keywords.is_command(tok, Keyword.theory))) element_depth
    2.44 +      else if (command_depth.isDefined) command_depth.get
    2.45 +      else if (command1) after_span_depth
    2.46 +      else span_depth
    2.47 +
    2.48 +    val (span_depth1, after_span_depth1, element_depth1) =
    2.49 +      ((span_depth, after_span_depth, element_depth) /: tokens) {
    2.50 +        case (depths @ (x, y, z), tok) =>
    2.51 +          if (tok.is_begin) (z + 2, z + 1, z + 1)
    2.52 +          else if (tok.is_end) (z + 1, z - 1, z - 1)
    2.53 +          else if (tok.is_command) {
    2.54 +            val depth0 = element_depth
    2.55 +            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
    2.56 +            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
    2.57 +            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
    2.58 +            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
    2.59 +            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
    2.60 +            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
    2.61 +            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
    2.62 +            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
    2.63 +            else depths
    2.64 +          }
    2.65 +          else depths
    2.66 +      }
    2.67 +
    2.68 +    Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    2.69 +  }
    2.70 +}
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Aug 03 11:45:09 2016 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Aug 04 10:55:51 2016 +0200
     3.3 @@ -44,22 +44,6 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* line-oriented structure */
     3.8 -
     3.9 -  object Line_Structure
    3.10 -  {
    3.11 -    val init = Line_Structure()
    3.12 -  }
    3.13 -
    3.14 -  sealed case class Line_Structure(
    3.15 -    improper: Boolean = true,
    3.16 -    command: Boolean = false,
    3.17 -    depth: Int = 0,
    3.18 -    span_depth: Int = 0,
    3.19 -    after_span_depth: Int = 0,
    3.20 -    element_depth: Int = 0)
    3.21 -
    3.22 -
    3.23    /* overall document structure */
    3.24  
    3.25    sealed abstract class Document { def length: Int }
    3.26 @@ -155,59 +139,6 @@
    3.27  
    3.28    /** parsing **/
    3.29  
    3.30 -  /* line-oriented structure */
    3.31 -
    3.32 -  private val close_structure =
    3.33 -    Set(Keyword.NEXT_BLOCK, Keyword.QED_BLOCK, Keyword.PRF_CLOSE, Keyword.THY_END)
    3.34 -
    3.35 -  def line_structure(tokens: List[Token], structure: Outer_Syntax.Line_Structure)
    3.36 -    : Outer_Syntax.Line_Structure =
    3.37 -  {
    3.38 -    val improper1 = tokens.forall(_.is_improper)
    3.39 -    val command1 = tokens.exists(_.is_begin_or_command)
    3.40 -
    3.41 -    val command_depth =
    3.42 -      tokens.iterator.filter(_.is_proper).toStream.headOption match {
    3.43 -        case Some(tok) =>
    3.44 -          if (keywords.is_command(tok, close_structure))
    3.45 -            Some(structure.after_span_depth - 1)
    3.46 -          else None
    3.47 -        case None => None
    3.48 -      }
    3.49 -
    3.50 -    val depth0 = structure.element_depth
    3.51 -    val depth1 =
    3.52 -      if (tokens.exists(tok =>
    3.53 -            keywords.is_before_command(tok) ||
    3.54 -            !tok.is_end && keywords.is_command(tok, Keyword.theory))) depth0
    3.55 -      else if (command_depth.isDefined) command_depth.get
    3.56 -      else if (command1) structure.after_span_depth
    3.57 -      else structure.span_depth
    3.58 -
    3.59 -    val (span_depth1, after_span_depth1, element_depth1) =
    3.60 -      ((structure.span_depth, structure.after_span_depth, structure.element_depth) /: tokens) {
    3.61 -        case (depths @ (x, y, z), tok) =>
    3.62 -          if (tok.is_begin) (z + 2, z + 1, z + 1)
    3.63 -          else if (tok.is_end) (z + 1, z - 1, z - 1)
    3.64 -          else if (tok.is_command) {
    3.65 -            if (keywords.is_command(tok, Keyword.theory_goal)) (depth0 + 2, depth0 + 1, z)
    3.66 -            else if (keywords.is_command(tok, Keyword.theory)) (depth0 + 1, depth0, z)
    3.67 -            else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1, z)
    3.68 -            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1, z)
    3.69 -            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2, z)
    3.70 -            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1, z)
    3.71 -            else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1, z)
    3.72 -            else if (keywords.is_command(tok, Keyword.qed_global)) (depth0 + 1, depth0, z)
    3.73 -            else depths
    3.74 -          }
    3.75 -          else depths
    3.76 -      }
    3.77 -
    3.78 -    Outer_Syntax.Line_Structure(
    3.79 -      improper1, command1, depth1, span_depth1, after_span_depth1, element_depth1)
    3.80 -  }
    3.81 -
    3.82 -
    3.83    /* command spans */
    3.84  
    3.85    def parse_spans(toks: List[Token]): List[Command_Span.Span] =
     4.1 --- a/src/Pure/build-jars	Wed Aug 03 11:45:09 2016 +0200
     4.2 +++ b/src/Pure/build-jars	Thu Aug 04 10:55:51 2016 +0200
     4.3 @@ -50,6 +50,7 @@
     4.4    General/word.scala
     4.5    General/xz_file.scala
     4.6    Isar/keyword.scala
     4.7 +  Isar/line_structure.scala
     4.8    Isar/outer_syntax.scala
     4.9    Isar/parse.scala
    4.10    Isar/token.scala
     5.1 --- a/src/Tools/jEdit/src/token_markup.scala	Wed Aug 03 11:45:09 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Thu Aug 04 10:55:51 2016 +0200
     5.3 @@ -178,7 +178,7 @@
     5.4    object Line_Context
     5.5    {
     5.6      def init(mode: String): Line_Context =
     5.7 -      new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
     5.8 +      new Line_Context(mode, Some(Scan.Finished), Line_Structure.init)
     5.9  
    5.10      def prev(buffer: JEditBuffer, line: Int): Line_Context =
    5.11        if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
    5.12 @@ -202,7 +202,7 @@
    5.13    class Line_Context(
    5.14        val mode: String,
    5.15        val context: Option[Scan.Line_Context],
    5.16 -      val structure: Outer_Syntax.Line_Structure)
    5.17 +      val structure: Line_Structure)
    5.18      extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
    5.19    {
    5.20      def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
    5.21 @@ -406,7 +406,7 @@
    5.22  
    5.23              case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
    5.24                val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
    5.25 -              val structure1 = syntax.line_structure(tokens, structure)
    5.26 +              val structure1 = structure.update(syntax.keywords, tokens)
    5.27                val styled_tokens =
    5.28                  tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
    5.29                (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))