src/Pure/Thy/thy_syntax.scala
changeset 49414 d7b5fb2e9ca2
parent 48873 18b17f15bc62
child 49524 68796a77c42b
equal deleted inserted replaced
49413:8c9925d31617 49414:d7b5fb2e9ca2
    66 
    66 
    67 
    67 
    68       /* result structure */
    68       /* result structure */
    69 
    69 
    70       val spans = parse_spans(syntax.scan(text))
    70       val spans = parse_spans(syntax.scan(text))
    71       spans.foreach(span => add(Command(Document.no_id, node_name, span)))
    71       spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
    72       result()
    72       result()
    73     }
    73     }
    74   }
    74   }
    75 
    75 
    76 
    76 
   224       case Nil =>
   224       case Nil =>
   225         assert(spans2.isEmpty)
   225         assert(spans2.isEmpty)
   226         commands
   226         commands
   227       case cmd :: _ =>
   227       case cmd :: _ =>
   228         val hook = commands.prev(cmd)
   228         val hook = commands.prev(cmd)
   229         val inserted = spans2.map(span => Command(Document.new_id(), name, span))
   229         val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
   230         (commands /: cmds2)(_ - _).append_after(hook, inserted)
   230         (commands /: cmds2)(_ - _).append_after(hook, inserted)
   231     }
   231     }
   232   }
   232   }
   233 
   233 
   234 
   234