changeset 65361 | ecefb68dc21d |
parent 65317 | b9f5cd845616 |
child 65470 | a0f49174dbeb |
--- a/src/Pure/PIDE/session.scala Mon Apr 03 16:50:44 2017 +0200 +++ b/src/Pure/PIDE/session.scala Mon Apr 03 17:00:36 2017 +0200 @@ -191,7 +191,7 @@ def recent_syntax(name: Document.Node.Name): Outer_Syntax = global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse - resources.base.syntax + resources.session_base.syntax /* pipelined change parsing */