sidekick root data: set buffer length to avoid crash of initial caret move;
authorwenzelm
Sun Sep 06 22:27:32 2009 +0200 (2009-09-06)
changeset 347173f32e08bbb6c
parent 34716 b8f2b44529fd
child 34718 39e3039645ae
sidekick root data: set buffer length to avoid crash of initial caret move;
separate Markup_Node, Markup_Tree, Markup_Text;
added Markup_Text.flatten;
Command.type_at: null-free version;
eliminated Command.RootInfo;
simplified printing of TypeInfo, RefInfo;
added Command.content(Int, Int);
src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/prover/Command.scala
src/Tools/jEdit/src/prover/MarkupNode.scala
src/Tools/jEdit/src/prover/State.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Sep 06 16:21:01 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Sun Sep 06 22:27:32 2009 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4      while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
     1.5        val command = cmd.get
     1.6        for {
     1.7 -        markup <- command.highlight_node(document).flatten
     1.8 +        markup <- command.highlight(document).flatten
     1.9          command_start = command.start(document)
    1.10          abs_start = to(command_start + markup.start)
    1.11          abs_stop = to(command_start + markup.stop)
     2.1 --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sun Sep 06 16:21:01 2009 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sun Sep 06 22:27:32 2009 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4  import errorlist.DefaultErrorSource
     2.5  import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
     2.6  
     2.7 -import isabelle.prover.{Command, MarkupNode}
     2.8 +import isabelle.prover.{Command, Markup_Node}
     2.9  import isabelle.proofdocument.ProofDocument
    2.10  
    2.11  
    2.12 @@ -31,26 +31,28 @@
    2.13  
    2.14    def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    2.15    {
    2.16 +    implicit def int_to_pos(offset: Int): Position =
    2.17 +      new Position { def getOffset = offset; override def toString = offset.toString }
    2.18 +
    2.19      stopped = false
    2.20  
    2.21      val data = new SideKickParsedData(buffer.getName)
    2.22 +    val root = data.root
    2.23 +    data.getAsset(root).setEnd(buffer.getLength)
    2.24  
    2.25      val prover_setup = Isabelle.prover_setup(buffer)
    2.26      if (prover_setup.isDefined) {
    2.27        val document = prover_setup.get.theory_view.current_document()
    2.28        for (command <- document.commands if !stopped) {
    2.29 -        data.root.add(command.markup_root(document).
    2.30 -          swing_tree((node: MarkupNode) =>
    2.31 +        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
    2.32              {
    2.33 -              implicit def int2pos(offset: Int): Position =
    2.34 -                new Position { def getOffset = offset; override def toString = offset.toString }
    2.35 -
    2.36 +              val content = command.content(node.start, node.stop)
    2.37                val command_start = command.start(document)
    2.38                val id = command.id
    2.39  
    2.40                new DefaultMutableTreeNode(new IAsset {
    2.41                  override def getIcon: Icon = null
    2.42 -                override def getShortString: String = node.content
    2.43 +                override def getShortString: String = content
    2.44                  override def getLongString: String = node.info.toString
    2.45                  override def getName: String = id
    2.46                  override def setName(name: String) = ()
    2.47 @@ -58,14 +60,13 @@
    2.48                  override def getStart: Position = command_start + node.start
    2.49                  override def setEnd(end: Position) = ()
    2.50                  override def getEnd: Position = command_start + node.stop
    2.51 -                override def toString =
    2.52 -                  id + ": " + node.content + "[" + getStart + " - " + getEnd + "]"
    2.53 +                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    2.54                })
    2.55              }))
    2.56        }
    2.57 -      if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
    2.58 +      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    2.59      }
    2.60 -    else data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    2.61 +    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    2.62  
    2.63      data
    2.64    }
     3.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 16:21:01 2009 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 22:27:32 2009 +0200
     3.3 @@ -293,7 +293,7 @@
     3.4      document.command_at(offset) match {
     3.5        case Some(cmd) =>
     3.6          document.token_start(cmd.tokens.first)
     3.7 -        cmd.type_at(document, offset - cmd.start(document))
     3.8 +        cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
     3.9        case None => null
    3.10      }
    3.11    }
     4.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Sun Sep 06 16:21:01 2009 +0200
     4.2 +++ b/src/Tools/jEdit/src/prover/Command.scala	Sun Sep 06 22:27:32 2009 +0200
     4.3 @@ -19,7 +19,6 @@
     4.4  
     4.5  trait Accumulator extends Actor
     4.6  {
     4.7 -
     4.8    start() // start actor
     4.9  
    4.10    protected var _state: State
    4.11 @@ -44,19 +43,16 @@
    4.12      val FAILED = Value("FAILED")
    4.13    }
    4.14  
    4.15 -  case object RootInfo
    4.16    case class HighlightInfo(highlight: String) { override def toString = highlight }
    4.17 -  case class TypeInfo(type_kind: String) { override def toString = type_kind }
    4.18 +  case class TypeInfo(ty: String)
    4.19    case class RefInfo(file: Option[String], line: Option[Int],
    4.20 -    command_id: Option[String], offset: Option[Int]) {
    4.21 -      override def toString = (file, line, command_id, offset).toString
    4.22 -    }
    4.23 +    command_id: Option[String], offset: Option[Int])
    4.24  }
    4.25  
    4.26  
    4.27  class Command(
    4.28 -  val tokens: List[Token],
    4.29 -  val starts: Map[Token, Int],
    4.30 +    val tokens: List[Token],
    4.31 +    val starts: Map[Token, Int],
    4.32    change_receiver: Actor) extends Accumulator
    4.33  {
    4.34    require(!tokens.isEmpty)
    4.35 @@ -73,6 +69,7 @@
    4.36  
    4.37    val name = tokens.head.content
    4.38    val content: String = Token.string_from_tokens(tokens, starts)
    4.39 +  def content(i: Int, j: Int): String = content.substring(i, j)
    4.40    val symbol_index = new Symbol.Index(content)
    4.41  
    4.42    def start(doc: ProofDocument) = doc.token_start(tokens.first)
    4.43 @@ -85,15 +82,13 @@
    4.44  
    4.45    /* markup */
    4.46  
    4.47 -  lazy val empty_root_node =
    4.48 -    new MarkupNode(0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
    4.49 -      content, Command.RootInfo, Nil)
    4.50 +  lazy val empty_markup = new Markup_Text(Nil, content)
    4.51  
    4.52 -  def markup_node(begin: Int, end: Int, info: Any): MarkupNode =
    4.53 +  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
    4.54    {
    4.55      val start = symbol_index.decode(begin)
    4.56      val stop = symbol_index.decode(end)
    4.57 -    new MarkupNode(start, stop, content.substring(start, stop), info, Nil)
    4.58 +    new Markup_Tree(new Markup_Node(start, stop, info), Nil)
    4.59    }
    4.60  
    4.61  
    4.62 @@ -106,7 +101,7 @@
    4.63    def status(doc: ProofDocument) = cmd_state(doc).state.status
    4.64    def result_document(doc: ProofDocument) = cmd_state(doc).result_document
    4.65    def markup_root(doc: ProofDocument) = cmd_state(doc).markup_root
    4.66 -  def highlight_node(doc: ProofDocument) = cmd_state(doc).highlight_node
    4.67 +  def highlight(doc: ProofDocument) = cmd_state(doc).highlight
    4.68    def type_at(doc: ProofDocument, offset: Int) = cmd_state(doc).type_at(offset)
    4.69    def ref_at(doc: ProofDocument, offset: Int) = cmd_state(doc).ref_at(offset)
    4.70  }
    4.71 @@ -124,13 +119,13 @@
    4.72          case elems => XML.Elem("messages", Nil, elems)
    4.73        }, "style")
    4.74  
    4.75 -  def markup_root: MarkupNode =
    4.76 -    (command.state.markup_root /: state.markup_root.children)(_ + _)
    4.77 +  def markup_root: Markup_Text =
    4.78 +    (command.state.markup_root /: state.markup_root.markup)(_ + _)
    4.79  
    4.80 -  def type_at(pos: Int): String = state.type_at(pos)
    4.81 +  def type_at(pos: Int): Option[String] = state.type_at(pos)
    4.82  
    4.83 -  def ref_at(pos: Int): Option[MarkupNode] = state.ref_at(pos)
    4.84 +  def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
    4.85  
    4.86 -  def highlight_node: MarkupNode =
    4.87 -    (command.state.highlight_node /: state.highlight_node.children)(_ + _)
    4.88 +  def highlight: Markup_Text =
    4.89 +    (command.state.highlight /: state.highlight.markup)(_ + _)
    4.90  }
    4.91 \ No newline at end of file
     5.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Sep 06 16:21:01 2009 +0200
     5.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Sun Sep 06 22:27:32 2009 +0200
     5.3 @@ -12,78 +12,100 @@
     5.4  import isabelle.proofdocument.ProofDocument
     5.5  
     5.6  
     5.7 -class MarkupNode(val start: Int, val stop: Int, val content: String, val info: Any,
     5.8 -  val children: List[MarkupNode])
     5.9 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
    5.10  {
    5.11 +  def fits_into(that: Markup_Node): Boolean =
    5.12 +    that.start <= this.start && this.stop <= that.stop
    5.13 +}
    5.14 +
    5.15  
    5.16 -  def swing_tree(make_node: MarkupNode => DefaultMutableTreeNode): DefaultMutableTreeNode =
    5.17 -  {
    5.18 -    val node = make_node(this)
    5.19 -    children.foreach(node add _.swing_tree(make_node))
    5.20 -    node
    5.21 -  }
    5.22 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
    5.23 +{
    5.24 +  def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
    5.25  
    5.26 -  def set_children(new_children: List[MarkupNode]): MarkupNode =
    5.27 -    new MarkupNode(start, stop, content, info, new_children)
    5.28 +  private def add(branch: Markup_Tree) =   // FIXME avoid sort
    5.29 +    set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
    5.30  
    5.31 -  private def add(child: MarkupNode) =   // FIXME avoid sort?
    5.32 -    set_children ((child :: children) sort ((a, b) => a.start < b.start))
    5.33 -
    5.34 -  def remove(nodes: List[MarkupNode]) = set_children(children -- nodes)
    5.35 +  private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
    5.36  
    5.37 -  def fits_into(node: MarkupNode): Boolean =
    5.38 -    node.start <= this.start && this.stop <= node.stop
    5.39 -
    5.40 -  def + (new_child: MarkupNode): MarkupNode =
    5.41 +  def + (new_tree: Markup_Tree): Markup_Tree =
    5.42    {
    5.43 -    if (new_child fits_into this) {
    5.44 +    val new_node = new_tree.node
    5.45 +    if (new_node fits_into node) {
    5.46        var inserted = false
    5.47 -      val new_children =
    5.48 -        children.map(c =>
    5.49 -          if ((new_child fits_into c) && !inserted) {inserted = true; c + new_child}
    5.50 -          else c)
    5.51 +      val new_branches =
    5.52 +        branches.map(branch =>
    5.53 +          if ((new_node fits_into branch.node) && !inserted) {
    5.54 +            inserted = true
    5.55 +            branch + new_tree
    5.56 +          }
    5.57 +          else branch)
    5.58        if (!inserted) {
    5.59 -        // new_child did not fit into children of this
    5.60 -        // -> insert new_child between this and its children
    5.61 -        val fitting = children filter(_ fits_into new_child)
    5.62 -        (this remove fitting) add ((new_child /: fitting) (_ + _))
    5.63 +        // new_tree did not fit into children of this
    5.64 +        // -> insert between this and its branches
    5.65 +        val fitting = branches filter(_.node fits_into new_node)
    5.66 +        (this remove fitting) add ((new_tree /: fitting)(_ + _))
    5.67        }
    5.68 -      else this set_children new_children
    5.69 +      else set_branches(new_branches)
    5.70      }
    5.71      else {
    5.72 -      System.err.println("ignored nonfitting markup: " + new_child)
    5.73 +      System.err.println("ignored nonfitting markup: " + new_node)
    5.74        this
    5.75      }
    5.76    }
    5.77  
    5.78 -  def flatten: List[MarkupNode] = {
    5.79 -    var next_x = start
    5.80 -    if (children.isEmpty) List(this)
    5.81 +  def flatten: List[Markup_Node] =
    5.82 +  {
    5.83 +    var next_x = node.start
    5.84 +    if (branches.isEmpty) List(this.node)
    5.85      else {
    5.86 -      val filled_gaps = for {
    5.87 -        child <- children
    5.88 -        markups =
    5.89 -          if (next_x < child.start) {
    5.90 -            // FIXME proper content!?
    5.91 -            new MarkupNode(next_x, child.start, content, info, Nil) :: child.flatten
    5.92 -          }
    5.93 -          else child.flatten
    5.94 -        update = (next_x = child.stop)
    5.95 -        markup <- markups
    5.96 -      } yield markup
    5.97 -      if (next_x < stop)
    5.98 -        filled_gaps + new MarkupNode(next_x, stop, content, info, Nil) // FIXME proper content!?
    5.99 +      val filled_gaps =
   5.100 +        for {
   5.101 +          child <- branches
   5.102 +          markups =
   5.103 +            if (next_x < child.node.start)
   5.104 +              new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
   5.105 +            else child.flatten
   5.106 +          update = (next_x = child.node.stop)
   5.107 +          markup <- markups
   5.108 +        } yield markup
   5.109 +      if (next_x < node.stop)
   5.110 +        filled_gaps + new Markup_Node(next_x, node.stop, node.info)
   5.111        else filled_gaps
   5.112      }
   5.113    }
   5.114 +}
   5.115  
   5.116 -  def filter(p: MarkupNode => Boolean): List[MarkupNode] =
   5.117 +
   5.118 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
   5.119 +{
   5.120 +  private lazy val root =
   5.121 +    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
   5.122 +
   5.123 +  def + (new_tree: Markup_Tree): Markup_Text =
   5.124 +    new Markup_Text((root + new_tree).branches, content)
   5.125 +
   5.126 +  def filter(pred: Markup_Node => Boolean): Markup_Text =
   5.127    {
   5.128 -    val filtered = children.flatMap(_.filter(p))
   5.129 -    if (p(this)) List(this set_children(filtered))
   5.130 -    else filtered
   5.131 +    def filt(tree: Markup_Tree): List[Markup_Tree] =
   5.132 +    {
   5.133 +      val branches = tree.branches.flatMap(filt(_))
   5.134 +      if (pred(tree.node)) List(tree.set_branches(branches))
   5.135 +      else branches
   5.136 +    }
   5.137 +    new Markup_Text(markup.flatMap(filt(_)), content)
   5.138    }
   5.139  
   5.140 -  override def toString =
   5.141 -    "([" + start + " - " + stop + "] ( " + content + "): " + info.toString
   5.142 +  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
   5.143 +
   5.144 +  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
   5.145 +  {
   5.146 +    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
   5.147 +    {
   5.148 +      val node = swing_node(tree.node)
   5.149 +      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
   5.150 +      node
   5.151 +    }
   5.152 +    swing(root)
   5.153 +  }
   5.154  }
     6.1 --- a/src/Tools/jEdit/src/prover/State.scala	Sun Sep 06 16:21:01 2009 +0200
     6.2 +++ b/src/Tools/jEdit/src/prover/State.scala	Sun Sep 06 22:27:32 2009 +0200
     6.3 @@ -12,10 +12,10 @@
     6.4    val command: Command,
     6.5    val status: Command.Status.Value,
     6.6    rev_results: List[XML.Tree],
     6.7 -  val markup_root: MarkupNode)
     6.8 +  val markup_root: Markup_Text)
     6.9  {
    6.10    def this(command: Command) =
    6.11 -    this(command, Command.Status.UNPROCESSED, Nil, command.empty_root_node)
    6.12 +    this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
    6.13  
    6.14  
    6.15    /* content */
    6.16 @@ -26,42 +26,45 @@
    6.17    private def add_result(res: XML.Tree): State =
    6.18      new State(command, status, res :: rev_results, markup_root)
    6.19  
    6.20 -  private def add_markup(markup: MarkupNode): State =
    6.21 -    new State(command, status, rev_results, markup_root + markup)
    6.22 +  private def add_markup(node: Markup_Tree): State =
    6.23 +    new State(command, status, rev_results, markup_root + node)
    6.24  
    6.25    lazy val results = rev_results.reverse
    6.26  
    6.27  
    6.28    /* markup */
    6.29  
    6.30 -  lazy val highlight_node: MarkupNode =
    6.31 +  lazy val highlight: Markup_Text =
    6.32    {
    6.33      markup_root.filter(_.info match {
    6.34 -      case Command.RootInfo | Command.HighlightInfo(_) => true
    6.35 +      case Command.HighlightInfo(_) => true
    6.36        case _ => false
    6.37 -    }).head
    6.38 +    })
    6.39    }
    6.40  
    6.41 -  private lazy val types =
    6.42 +  private lazy val types: List[Markup_Node] =
    6.43      markup_root.filter(_.info match {
    6.44        case Command.TypeInfo(_) => true
    6.45 -      case _ => false }).flatten(_.flatten)
    6.46 +      case _ => false }).flatten
    6.47  
    6.48 -  def type_at(pos: Int): String =
    6.49 +  def type_at(pos: Int): Option[String] =
    6.50    {
    6.51 -    types.find(t => t.start <= pos && pos < t.stop).map(t =>
    6.52 -      t.content + ": " + (t.info match {
    6.53 -        case Command.TypeInfo(i) => i
    6.54 -        case _ => "" })).
    6.55 -      getOrElse(null)
    6.56 +    types.find(t => t.start <= pos && pos < t.stop) match {
    6.57 +      case Some(t) =>
    6.58 +        t.info match {
    6.59 +          case Command.TypeInfo(ty) => Some(command.content(t.start, t.stop) + ": " + ty)
    6.60 +          case _ => None
    6.61 +        }
    6.62 +      case None => None
    6.63 +    }
    6.64    }
    6.65  
    6.66 -  private lazy val refs =
    6.67 +  private lazy val refs: List[Markup_Node] =
    6.68      markup_root.filter(_.info match {
    6.69        case Command.RefInfo(_, _, _, _) => true
    6.70 -      case _ => false }).flatten(_.flatten)
    6.71 +      case _ => false }).flatten
    6.72  
    6.73 -  def ref_at(pos: Int): Option[MarkupNode] =
    6.74 +  def ref_at(pos: Int): Option[Markup_Node] =
    6.75      refs.find(t => t.start <= pos && pos < t.stop)
    6.76  
    6.77