71 { |
71 { |
72 /* header */ |
72 /* header */ |
73 |
73 |
74 def is_theory: Boolean = node_name.is_theory |
74 def is_theory: Boolean = node_name.is_theory |
75 |
75 |
76 def is_ml_root: Boolean = |
|
77 Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory }) |
|
78 |
|
79 def is_bootstrap_thy: Boolean = |
|
80 Thy_Header.bootstrap_thys.exists({ case (_, name) => name == node_name.theory }) |
|
81 |
|
82 def node_header(): Document.Node.Header = |
76 def node_header(): Document.Node.Header = |
83 { |
77 { |
84 GUI_Thread.require {} |
78 GUI_Thread.require {} |
85 |
79 |
86 if (is_ml_root) |
80 PIDE.resources.special_header(node_name) getOrElse |
87 Document.Node.Header( |
81 { |
88 List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none))) |
82 if (is_theory) { |
89 else if (is_theory) { |
|
90 if (is_bootstrap_thy) { |
|
91 Document.Node.Header( |
|
92 List((PIDE.resources.import_name("", node_name, Thy_Header.PURE), Position.none))) |
|
93 } |
|
94 else { |
|
95 JEdit_Lib.buffer_lock(buffer) { |
83 JEdit_Lib.buffer_lock(buffer) { |
96 Token_Markup.line_token_iterator( |
84 Token_Markup.line_token_iterator( |
97 Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst( |
85 Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst( |
98 { |
86 { |
99 case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start |
87 case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start |
101 match { |
89 match { |
102 case Some(offset) => |
90 case Some(offset) => |
103 val length = buffer.getLength - offset |
91 val length = buffer.getLength - offset |
104 PIDE.resources.check_thy_reader("", node_name, |
92 PIDE.resources.check_thy_reader("", node_name, |
105 new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command) |
93 new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command) |
106 case None => Document.Node.no_header |
94 case None => |
|
95 Document.Node.no_header |
107 } |
96 } |
108 } |
97 } |
109 } |
98 } |
110 } |
99 else Document.Node.no_header |
111 else Document.Node.no_header |
100 } |
112 } |
101 } |
113 |
102 |
114 |
103 |
115 /* perspective */ |
104 /* perspective */ |
116 |
105 |