changeset 67004 | af72fa58f71b |
parent 66984 | a1d3e5df0c95 |
child 67014 | e6a695d6a6b2 |
--- a/src/Tools/VSCode/src/document_model.scala Sat Nov 04 15:24:40 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sat Nov 04 17:11:21 2017 +0100 @@ -240,5 +240,5 @@ /* syntax */ def syntax(): Outer_Syntax = - if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.init + if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty }