clarified Line_Structure wrt. command span;
authorwenzelm
Sat Oct 18 20:56:16 2014 +0200 (2014-10-18)
changeset 587004717d18cc619
parent 58699 e46afcceb781
child 58701 cc83453fac15
clarified Line_Structure wrt. command span;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/fold_handling.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 11:19:34 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 20:56:16 2014 +0200
     1.3 @@ -43,10 +43,15 @@
     1.4  
     1.5    object Line_Structure
     1.6    {
     1.7 -    val init = Line_Structure(0, 0)
     1.8 +    val init = Line_Structure()
     1.9    }
    1.10  
    1.11 -  sealed case class Line_Structure(depth_before: Int, depth: Int)
    1.12 +  sealed case class Line_Structure(
    1.13 +    improper: Boolean = true,
    1.14 +    command: Boolean = false,
    1.15 +    depth: Int = 0,
    1.16 +    span_depth: Int = 0,
    1.17 +    after_span_depth: Int = 0)
    1.18  }
    1.19  
    1.20  final class Outer_Syntax private(
    1.21 @@ -150,21 +155,29 @@
    1.22  
    1.23    /* line-oriented structure */
    1.24  
    1.25 -  def line_structure(tokens: List[Token], depth: Int): Outer_Syntax.Line_Structure =
    1.26 +  def line_structure(tokens: List[Token], struct: Outer_Syntax.Line_Structure)
    1.27 +    : Outer_Syntax.Line_Structure =
    1.28    {
    1.29 +    val improper1 = tokens.forall(_.is_improper)
    1.30 +    val command1 = tokens.exists(_.is_command)
    1.31 +
    1.32      val depth1 =
    1.33        if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0
    1.34 -      else depth
    1.35 -    val depth2 =
    1.36 -      (depth /: tokens) { case (d, tok) =>
    1.37 -        if (command_kind(tok, Keyword.theory_goal)) 1
    1.38 -        else if (command_kind(tok, Keyword.theory)) 0
    1.39 -        else if (command_kind(tok, Keyword.proof_goal)) d + 1
    1.40 -        else if (command_kind(tok, Keyword.qed)) d - 1
    1.41 -        else if (command_kind(tok, Keyword.qed_global)) 0
    1.42 -        else d
    1.43 +      else if (command1) struct.after_span_depth
    1.44 +      else struct.span_depth
    1.45 +
    1.46 +    val (span_depth1, after_span_depth1) =
    1.47 +      ((struct.span_depth, struct.after_span_depth) /: tokens) {
    1.48 +        case ((d0, d), tok) =>
    1.49 +          if (command_kind(tok, Keyword.theory_goal)) (2, 1)
    1.50 +          else if (command_kind(tok, Keyword.theory)) (1, 0)
    1.51 +          else if (command_kind(tok, Keyword.proof_goal)) (d + 2, d + 1)
    1.52 +          else if (command_kind(tok, Keyword.qed)) (d + 1, d - 1)
    1.53 +          else if (command_kind(tok, Keyword.qed_global)) (1, 0)
    1.54 +          else (d0, d)
    1.55        }
    1.56 -    Outer_Syntax.Line_Structure(depth1, depth2)
    1.57 +
    1.58 +    Outer_Syntax.Line_Structure(improper1, command1, depth1, span_depth1, after_span_depth1)
    1.59    }
    1.60  
    1.61  
    1.62 @@ -197,7 +210,7 @@
    1.63        }
    1.64      }
    1.65      val tokens = toks.toList
    1.66 -    (tokens, ctxt, line_structure(tokens, structure.depth))
    1.67 +    (tokens, ctxt, line_structure(tokens, structure))
    1.68    }
    1.69  
    1.70  
     2.1 --- a/src/Tools/jEdit/src/fold_handling.scala	Sat Oct 18 11:19:34 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/fold_handling.scala	Sat Oct 18 20:56:16 2014 +0200
     2.3 @@ -9,9 +9,11 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 -import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
     2.8 +import javax.swing.text.Segment
     2.9  
    2.10 -import javax.swing.text.Segment
    2.11 +import scala.collection.convert.WrapAsJava
    2.12 +
    2.13 +import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
    2.14  
    2.15  
    2.16  object Fold_Handling
    2.17 @@ -27,7 +29,22 @@
    2.18        }
    2.19  
    2.20      override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
    2.21 -      Token_Markup.buffer_line_structure(buffer, line).depth_before
    2.22 +      Token_Markup.buffer_line_structure(buffer, line).depth max 0
    2.23 +
    2.24 +    override def getPrecedingFoldLevels(
    2.25 +      buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
    2.26 +    {
    2.27 +      val struct = Token_Markup.buffer_line_structure(buffer, line)
    2.28 +      val result =
    2.29 +        if (line > 0 && struct.command)
    2.30 +          Range.inclusive(line - 1, 0, -1).iterator.
    2.31 +            map(Token_Markup.buffer_line_structure(buffer, _)).
    2.32 +            takeWhile(_.improper).map(_ => struct.depth max 0).toList
    2.33 +        else Nil
    2.34 +
    2.35 +      if (result.isEmpty) null
    2.36 +      else WrapAsJava.seqAsJavaList(result.map(i => new Integer(i)))
    2.37 +    }
    2.38    }
    2.39  
    2.40