changeset 54509 | 1f77110c94ef |
parent 54462 | c9bb76303348 |
child 54513 | 5545aff878b1 |
--- a/src/Pure/Thy/thy_syntax.scala Mon Nov 18 09:45:50 2013 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Mon Nov 18 17:16:56 2013 +0100 @@ -355,6 +355,8 @@ else node.update_perspective(perspective).update_commands( consolidate_spans(syntax, reparse_limit, name, visible, node.commands)) + + case (_, Document.Node.Blob(blob)) => node.update_blob(blob) } }