basic support for outer syntax keywords in theory header;
authorwenzelm
Thu Mar 15 14:13:49 2012 +0100 (2012-03-15)
changeset 46942f5c2d66faa04
parent 46941 c0f776b661fa
child 46943 ac1c41ea856d
basic support for outer syntax keywords in theory header;
src/HOL/Library/Old_Recdef.thy
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     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 {