src/Pure/Thy/thy_syntax.scala
changeset 66770 122df1fde073
parent 66721 ae38b8c0fdd9
child 66772 a66f11a0b5b1
equal deleted inserted replaced
66769:97f16ada519c 66770:122df1fde073
   100         if (node.is_empty) None
   100         if (node.is_empty) None
   101         else {
   101         else {
   102           val header = node.header
   102           val header = node.header
   103           val imports_syntax =
   103           val imports_syntax =
   104             Outer_Syntax.merge(
   104             Outer_Syntax.merge(
   105               header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
   105               header.imports.map(p => resources.session_base.node_syntax(nodes, p._1)))
   106           Some(imports_syntax + header)
   106           Some(imports_syntax + header)
   107         }
   107         }
   108       nodes += (name -> node.update_syntax(syntax))
   108       nodes += (name -> node.update_syntax(syntax))
   109     }
   109     }
   110 
   110 
   323             .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   323             .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
   324 
   324 
   325         node_edits foreach {
   325         node_edits foreach {
   326           case (name, edits) =>
   326           case (name, edits) =>
   327             val node = nodes(name)
   327             val node = nodes(name)
   328             val syntax =
   328             val syntax = resources.session_base.node_syntax(nodes, name)
   329               resources.session_base.node_syntax(nodes, name) getOrElse
       
   330               Thy_Header.bootstrap_syntax
       
   331             val commands = node.commands
   329             val commands = node.commands
   332 
   330 
   333             val node1 =
   331             val node1 =
   334               if (reparse_set(name) && commands.nonEmpty)
   332               if (reparse_set(name) && commands.nonEmpty)
   335                 node.update_commands(
   333                 node.update_commands(