1.1 --- a/src/HOL/Library/Old_Recdef.thy Thu Mar 15 11:37:56 2012 +0100
1.2 +++ b/src/HOL/Library/Old_Recdef.thy Thu Mar 15 14:13:49 2012 +0100
1.3 @@ -6,6 +6,7 @@
1.4
1.5 theory Old_Recdef
1.6 imports Wfrec
1.7 +keywords "recdef" :: thy_decl
1.8 uses
1.9 ("~~/src/HOL/Tools/TFL/casesplit.ML")
1.10 ("~~/src/HOL/Tools/TFL/utils.ML")
2.1 --- a/src/Pure/PIDE/document.scala Thu Mar 15 11:37:56 2012 +0100
2.2 +++ b/src/Pure/PIDE/document.scala Thu Mar 15 14:13:49 2012 +0100
2.3 @@ -122,6 +122,12 @@
2.4 def update_commands(new_commands: Linear_Set[Command]): Node =
2.5 new Node(header, perspective, blobs, new_commands)
2.6
2.7 + def imports: List[Node.Name] =
2.8 + header match { case Exn.Res(deps) => deps.imports case _ => Nil }
2.9 +
2.10 + def keywords: List[Outer_Syntax.Decl] =
2.11 + header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
2.12 +
2.13
2.14 /* commands */
2.15
2.16 @@ -184,11 +190,7 @@
2.17 def + (entry: (Node.Name, Node)): Nodes =
2.18 {
2.19 val (name, node) = entry
2.20 - val imports =
2.21 - node.header match {
2.22 - case Exn.Res(deps) => deps.imports
2.23 - case _ => Nil
2.24 - }
2.25 + val imports = node.imports
2.26 val graph1 =
2.27 (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
2.28 val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
2.29 @@ -199,6 +201,7 @@
2.30 def entries: Iterator[(Node.Name, Node)] =
2.31 graph.entries.map({ case (name, (node, _)) => (name, node) })
2.32
2.33 + def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
2.34 def topological_order: List[Node.Name] = graph.topological_order
2.35 }
2.36
3.1 --- a/src/Pure/System/session.scala Thu Mar 15 11:37:56 2012 +0100
3.2 +++ b/src/Pure/System/session.scala Thu Mar 15 14:13:49 2012 +0100
3.3 @@ -100,8 +100,7 @@
3.4
3.5 case Text_Edits(name, previous, text_edits, version_result) =>
3.6 val prev = previous.get_finished
3.7 - val syntax = if (prev.is_init) prover_syntax else prev.syntax
3.8 - val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits)
3.9 + val (doc_edits, version) = Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
3.10 version_result.fulfill(version)
3.11 sender ! Change_Node(name, doc_edits, prev, version)
3.12
4.1 --- a/src/Pure/Thy/thy_syntax.scala Thu Mar 15 11:37:56 2012 +0100
4.2 +++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 15 14:13:49 2012 +0100
4.3 @@ -145,7 +145,7 @@
4.4 /** text edits **/
4.5
4.6 def text_edits(
4.7 - syntax: Outer_Syntax,
4.8 + base_syntax: Outer_Syntax,
4.9 previous: Document.Version,
4.10 edits: List[Document.Edit_Text])
4.11 : (List[Document.Edit_Command], Document.Version) =
4.12 @@ -181,8 +181,10 @@
4.13
4.14 /* phase 2: recover command spans */
4.15
4.16 - @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command])
4.17 - : Linear_Set[Command] =
4.18 + @tailrec def recover_spans(
4.19 + syntax: Outer_Syntax,
4.20 + node_name: Document.Node.Name,
4.21 + commands: Linear_Set[Command]): Linear_Set[Command] =
4.22 {
4.23 commands.iterator.find(cmd => !cmd.is_defined) match {
4.24 case Some(first_unparsed) =>
4.25 @@ -211,7 +213,7 @@
4.26 val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
4.27 val new_commands =
4.28 commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
4.29 - recover_spans(node_name, new_commands)
4.30 + recover_spans(syntax, node_name, new_commands)
4.31
4.32 case None => commands
4.33 }
4.34 @@ -223,8 +225,34 @@
4.35 {
4.36 val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
4.37 var nodes = previous.nodes
4.38 + var rebuild_syntax = previous.is_init
4.39
4.40 + // structure and syntax
4.41 edits foreach {
4.42 + case (name, Document.Node.Header(header)) =>
4.43 + val node = nodes(name)
4.44 + val update_header =
4.45 + (node.header, header) match {
4.46 + case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
4.47 + case _ => true
4.48 + }
4.49 + if (update_header) {
4.50 + doc_edits += (name -> Document.Node.Header(header))
4.51 + val node1 = node.update_header(header)
4.52 + nodes += (name -> node1)
4.53 + rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords)
4.54 + }
4.55 +
4.56 + case _ =>
4.57 + }
4.58 +
4.59 + val syntax =
4.60 + if (rebuild_syntax)
4.61 + (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
4.62 + else previous.syntax
4.63 +
4.64 + // node content
4.65 + edits foreach { // FIXME observe rebuild_syntax!?
4.66 case (name, Document.Node.Clear()) =>
4.67 doc_edits += (name -> Document.Node.Clear())
4.68 nodes += (name -> nodes(name).clear)
4.69 @@ -233,7 +261,7 @@
4.70 val node = nodes(name)
4.71 val commands0 = node.commands
4.72 val commands1 = edit_text(text_edits, commands0)
4.73 - val commands2 = recover_spans(name, commands1) // FIXME somewhat slow
4.74 + val commands2 = recover_spans(syntax, name, commands1) // FIXME somewhat slow
4.75
4.76 val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
4.77 val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
4.78 @@ -245,17 +273,7 @@
4.79 doc_edits += (name -> Document.Node.Edits(cmd_edits))
4.80 nodes += (name -> node.update_commands(commands2))
4.81
4.82 - case (name, Document.Node.Header(header)) =>
4.83 - val node = nodes(name)
4.84 - val update_header =
4.85 - (node.header, header) match {
4.86 - case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
4.87 - case _ => true
4.88 - }
4.89 - if (update_header) {
4.90 - doc_edits += (name -> Document.Node.Header(header))
4.91 - nodes += (name -> node.update_header(header))
4.92 - }
4.93 + case (name, Document.Node.Header(_)) =>
4.94
4.95 case (name, Document.Node.Perspective(text_perspective)) =>
4.96 update_perspective(nodes, name, text_perspective) match {