src/Pure/Thy/thy_syntax.scala
changeset 82788 5afb8d0d418e
parent 82787 ddb68e3058d3
child 82789 941b6cdf3611
equal deleted inserted replaced
82787:ddb68e3058d3 82788:5afb8d0d418e
   326         val reparse_set = reparse.toSet
   326         val reparse_set = reparse.toSet
   327 
   327 
   328         var nodes = nodes0
   328         var nodes = nodes0
   329         val doc_edits = mutable.ListBuffer.from(doc_edits0)
   329         val doc_edits = mutable.ListBuffer.from(doc_edits0)
   330 
   330 
   331         val node_edits =
   331         val node_edits = (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
   332           (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
       
   333             .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
       
   334 
   332 
   335         node_edits foreach {
   333         node_edits foreach {
   336           case (name, edits) =>
   334           case (name, edits) =>
   337             val node = nodes(name)
   335             val node = nodes(name)
   338             val syntax = session_base.node_syntax(nodes, name)
   336             val syntax = session_base.node_syntax(nodes, name)