equal
deleted
inserted
replaced
94 else { |
94 else { |
95 JEdit_Lib.buffer_lock(buffer) { |
95 JEdit_Lib.buffer_lock(buffer) { |
96 Token_Markup.line_token_iterator( |
96 Token_Markup.line_token_iterator( |
97 Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst( |
97 Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst( |
98 { |
98 { |
99 case Text.Info(range, tok) |
99 case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start |
100 if tok.is_command && tok.source == Thy_Header.THEORY => range.start |
|
101 }) |
100 }) |
102 match { |
101 match { |
103 case Some(offset) => |
102 case Some(offset) => |
104 val length = buffer.getLength - offset |
103 val length = buffer.getLength - offset |
105 PIDE.resources.check_thy_reader("", node_name, |
104 PIDE.resources.check_thy_reader("", node_name, |