# HG changeset patch
# User wenzelm
# Date 1348317701 -7200
# Node ID 68796a77c42bc1ab37fa2718da77acd529615246
# Parent  dc06703640082ec753a5be88cdf68e2aa43fe0d7
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;

diff -r dc0670364008 -r 68796a77c42b etc/options
--- a/etc/options	Sat Sep 22 14:03:01 2012 +0200
+++ b/etc/options	Sat Sep 22 14:41:41 2012 +0200
@@ -95,3 +95,5 @@
 option editor_update_delay : real = 0.5
   -- "delay for physical GUI updates"
 
+option editor_reparse_limit : int = 10000
+  -- "maximum amount of reparsed text outside perspective"
diff -r dc0670364008 -r 68796a77c42b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Sep 22 14:03:01 2012 +0200
+++ b/src/Pure/System/session.scala	Sat Sep 22 14:41:41 2012 +0200
@@ -53,6 +53,7 @@
   def prune_delay: Time = Time.seconds(60.0)  // prune history -- delete old versions
   def prune_size: Int = 0  // size of retained history
   def syslog_limit: Int = 100
+  def reparse_limit: Int = 0
 
 
   /* pervasive event buses */
@@ -107,7 +108,7 @@
           val prev = previous.get_finished
           val (doc_edits, version) =
             Timing.timeit("Thy_Syntax.text_edits", timing) {
-              Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
+              Thy_Syntax.text_edits(thy_load.base_syntax, reparse_limit, prev, text_edits)
             }
           version_result.fulfill(version)
           sender ! Change(doc_edits, prev, version)
diff -r dc0670364008 -r 68796a77c42b src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sat Sep 22 14:03:01 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sat Sep 22 14:41:41 2012 +0200
@@ -263,6 +263,7 @@
 
   private def consolidate_spans(
     syntax: Outer_Syntax,
+    reparse_limit: Int,
     name: Document.Node.Name,
     perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -274,7 +275,14 @@
           val visible = perspective.commands.toSet
           commands.reverse.find(visible) match {
             case Some(last_visible) =>
-              reparse_spans(syntax, name, commands, first_unfinished, last_visible)
+              val it = commands.iterator(last_visible)
+              var last = last_visible
+              var i = 0
+              while (i < reparse_limit && it.hasNext) {
+                last = it.next
+                i += last.length
+              }
+              reparse_spans(syntax, name, commands, first_unfinished, last)
             case None => commands
           }
         case None => commands
@@ -295,7 +303,7 @@
     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   }
 
-  private def text_edit(syntax: Outer_Syntax,
+  private def text_edit(syntax: Outer_Syntax, reparse_limit: Int,
     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   {
     edit match {
@@ -313,13 +321,14 @@
         val perspective = command_perspective(node, text_perspective)
         if (node.perspective same perspective) node
         else
-          node.update_perspective(perspective)
-            .update_commands(consolidate_spans(syntax, name, perspective, node.commands))
+          node.update_perspective(perspective).update_commands(
+            consolidate_spans(syntax, reparse_limit, name, perspective, node.commands))
     }
   }
 
   def text_edits(
       base_syntax: Outer_Syntax,
+      reparse_limit: Int,
       previous: Document.Version,
       edits: List[Document.Edit_Text])
     : (List[Document.Edit_Command], Document.Version) =
@@ -343,7 +352,7 @@
           if (reparse_set(name) && !commands.isEmpty)
             node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
           else node
-        val node2 = (node1 /: edits)(text_edit(syntax, _, _))
+        val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
 
         if (!(node.perspective same node2.perspective))
           doc_edits += (name -> Document.Node.Perspective(node2.perspective))
diff -r dc0670364008 -r 68796a77c42b src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Sep 22 14:03:01 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Sep 22 14:41:41 2012 +0200
@@ -43,7 +43,7 @@
   private val relevant_options =
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
       "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
-      "editor_input_delay", "editor_output_delay", "editor_update_delay")
+      "editor_input_delay", "editor_output_delay", "editor_update_delay", "editor_reparse_limit")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 
diff -r dc0670364008 -r 68796a77c42b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 22 14:03:01 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 22 14:41:41 2012 +0200
@@ -344,8 +344,10 @@
 
       val content = Isabelle_Logic.session_content(false)
       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
+
       Isabelle.session = new Session(thy_load) {
         override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
+        override def reparse_limit = Isabelle.options.int("editor_reparse_limit")
       }
 
       Isabelle.session.phase_changed += session_manager