equal
deleted
inserted
replaced
78 else None |
78 else None |
79 } |
79 } |
80 else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) |
80 else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) |
81 case None => |
81 case None => |
82 PIDE.document_model(buffer) match { |
82 PIDE.document_model(buffer) match { |
83 case Some(model) if !model.node_name.is_theory => |
83 case Some(model) if !model.is_theory => |
84 snapshot.version.nodes.thy_load_commands(model.node_name) match { |
84 snapshot.version.nodes.thy_load_commands(model.node_name) match { |
85 case cmd :: _ => Some(cmd) |
85 case cmd :: _ => Some(cmd) |
86 case Nil => None |
86 case Nil => None |
87 } |
87 } |
88 case _ => None |
88 case _ => None |