Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
authorwenzelm
Sat Sep 22 14:41:41 2012 +0200 (2012-09-22)
changeset 4952468796a77c42b
parent 49523 dc0670364008
child 49525 e87b42a26991
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
etc/options
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/etc/options	Sat Sep 22 14:03:01 2012 +0200
     1.2 +++ b/etc/options	Sat Sep 22 14:41:41 2012 +0200
     1.3 @@ -95,3 +95,5 @@
     1.4  option editor_update_delay : real = 0.5
     1.5    -- "delay for physical GUI updates"
     1.6  
     1.7 +option editor_reparse_limit : int = 10000
     1.8 +  -- "maximum amount of reparsed text outside perspective"
     2.1 --- a/src/Pure/System/session.scala	Sat Sep 22 14:03:01 2012 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Sep 22 14:41:41 2012 +0200
     2.3 @@ -53,6 +53,7 @@
     2.4    def prune_delay: Time = Time.seconds(60.0)  // prune history -- delete old versions
     2.5    def prune_size: Int = 0  // size of retained history
     2.6    def syslog_limit: Int = 100
     2.7 +  def reparse_limit: Int = 0
     2.8  
     2.9  
    2.10    /* pervasive event buses */
    2.11 @@ -107,7 +108,7 @@
    2.12            val prev = previous.get_finished
    2.13            val (doc_edits, version) =
    2.14              Timing.timeit("Thy_Syntax.text_edits", timing) {
    2.15 -              Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
    2.16 +              Thy_Syntax.text_edits(thy_load.base_syntax, reparse_limit, prev, text_edits)
    2.17              }
    2.18            version_result.fulfill(version)
    2.19            sender ! Change(doc_edits, prev, version)
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Sep 22 14:03:01 2012 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Sep 22 14:41:41 2012 +0200
     3.3 @@ -263,6 +263,7 @@
     3.4  
     3.5    private def consolidate_spans(
     3.6      syntax: Outer_Syntax,
     3.7 +    reparse_limit: Int,
     3.8      name: Document.Node.Name,
     3.9      perspective: Command.Perspective,
    3.10      commands: Linear_Set[Command]): Linear_Set[Command] =
    3.11 @@ -274,7 +275,14 @@
    3.12            val visible = perspective.commands.toSet
    3.13            commands.reverse.find(visible) match {
    3.14              case Some(last_visible) =>
    3.15 -              reparse_spans(syntax, name, commands, first_unfinished, last_visible)
    3.16 +              val it = commands.iterator(last_visible)
    3.17 +              var last = last_visible
    3.18 +              var i = 0
    3.19 +              while (i < reparse_limit && it.hasNext) {
    3.20 +                last = it.next
    3.21 +                i += last.length
    3.22 +              }
    3.23 +              reparse_spans(syntax, name, commands, first_unfinished, last)
    3.24              case None => commands
    3.25            }
    3.26          case None => commands
    3.27 @@ -295,7 +303,7 @@
    3.28      inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
    3.29    }
    3.30  
    3.31 -  private def text_edit(syntax: Outer_Syntax,
    3.32 +  private def text_edit(syntax: Outer_Syntax, reparse_limit: Int,
    3.33      node: Document.Node, edit: Document.Edit_Text): Document.Node =
    3.34    {
    3.35      edit match {
    3.36 @@ -313,13 +321,14 @@
    3.37          val perspective = command_perspective(node, text_perspective)
    3.38          if (node.perspective same perspective) node
    3.39          else
    3.40 -          node.update_perspective(perspective)
    3.41 -            .update_commands(consolidate_spans(syntax, name, perspective, node.commands))
    3.42 +          node.update_perspective(perspective).update_commands(
    3.43 +            consolidate_spans(syntax, reparse_limit, name, perspective, node.commands))
    3.44      }
    3.45    }
    3.46  
    3.47    def text_edits(
    3.48        base_syntax: Outer_Syntax,
    3.49 +      reparse_limit: Int,
    3.50        previous: Document.Version,
    3.51        edits: List[Document.Edit_Text])
    3.52      : (List[Document.Edit_Command], Document.Version) =
    3.53 @@ -343,7 +352,7 @@
    3.54            if (reparse_set(name) && !commands.isEmpty)
    3.55              node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
    3.56            else node
    3.57 -        val node2 = (node1 /: edits)(text_edit(syntax, _, _))
    3.58 +        val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
    3.59  
    3.60          if (!(node.perspective same node2.perspective))
    3.61            doc_edits += (name -> Document.Node.Perspective(node2.perspective))
     4.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Sep 22 14:03:01 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Sep 22 14:41:41 2012 +0200
     4.3 @@ -43,7 +43,7 @@
     4.4    private val relevant_options =
     4.5      Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
     4.6        "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
     4.7 -      "editor_input_delay", "editor_output_delay", "editor_update_delay")
     4.8 +      "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
     4.9  
    4.10    relevant_options.foreach(Isabelle.options.value.check_name _)
    4.11  
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 22 14:03:01 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 22 14:41:41 2012 +0200
     5.3 @@ -344,8 +344,10 @@
     5.4  
     5.5        val content = Isabelle_Logic.session_content(false)
     5.6        val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
     5.7 +
     5.8        Isabelle.session = new Session(thy_load) {
     5.9          override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
    5.10 +        override def reparse_limit = Isabelle.options.int("editor_reparse_limit")
    5.11        }
    5.12  
    5.13        Isabelle.session.phase_changed += session_manager