1/* Title: Tools/jEdit/src/isabelle_sidekick.scala 2 Author: Fabian Immler, TU Munich 3 Author: Makarius 4 5SideKick parsers for Isabelle proof documents. 6*/ 7 8package isabelle.jedit 9 10 11import isabelle._ 12 13import javax.swing.tree.DefaultMutableTreeNode 14import javax.swing.text.Position 15import javax.swing.{JLabel, Icon} 16 17import org.gjt.sp.jedit.Buffer 18import sidekick.{SideKickParser, SideKickParsedData, IAsset} 19 20 21object Isabelle_Sidekick 22{ 23 def int_to_pos(offset: Text.Offset): Position = 24 new Position { def getOffset = offset; override def toString: String = offset.toString } 25 26 def root_data(buffer: Buffer): SideKickParsedData = 27 { 28 val data = new SideKickParsedData(buffer.getName) 29 data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength)) 30 data 31 } 32 33 class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset 34 { 35 private val css = GUI.imitate_font_css(GUI.label_font()) 36 37 protected var _name = text 38 protected var _start = int_to_pos(range.start) 39 protected var _end = int_to_pos(range.stop) 40 override def getIcon: Icon = null 41 override def getShortString: String = 42 { 43 val n = keyword.length 44 val s = 45 _name.indexOf(keyword) match { 46 case i if i >= 0 && n > 0 => 47 HTML.output(_name.substring(0, i)) + 48 "<b>" + HTML.output(keyword) + "</b>" + 49 HTML.output(_name.substring(i + n)) 50 case _ => HTML.output(_name) 51 } 52 "<html><span style=\"" + css + "\">" + s + "</span></html>" 53 } 54 override def getLongString: String = _name 55 override def getName: String = _name 56 override def setName(name: String) = _name = name 57 override def getStart: Position = _start 58 override def setStart(start: Position) = _start = start 59 override def getEnd: Position = _end 60 override def setEnd(end: Position) = _end = end 61 override def toString: String = _name 62 } 63 64 class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range) 65 66 def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode, 67 swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode) 68 { 69 for ((_, entry) <- tree.branches) { 70 val node = swing_node(Text.Info(entry.range, entry.markup)) 71 swing_markup_tree(entry.subtree, node, swing_node) 72 parent.add(node) 73 } 74 } 75} 76 77 78class Isabelle_Sidekick(name: String) extends SideKickParser(name) 79{ 80 override def supportsCompletion = false 81 82 83 /* parsing */ 84 85 @volatile protected var stopped = false 86 override def stop() = { stopped = true } 87 88 def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false 89 90 def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = 91 { 92 stopped = false 93 94 // FIXME lock buffer (!??) 95 val data = Isabelle_Sidekick.root_data(buffer) 96 val syntax = Isabelle.buffer_syntax(buffer) 97 val ok = 98 if (syntax.isDefined) { 99 val ok = parser(buffer, syntax.get, data) 100 if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true } 101 else ok 102 } 103 else false 104 if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>")) 105 106 data 107 } 108} 109 110 111class Isabelle_Sidekick_Structure( 112 name: String, 113 node_name: Buffer => Option[Document.Node.Name], 114 parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document]) 115 extends Isabelle_Sidekick(name) 116{ 117 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = 118 { 119 def make_tree( 120 parent: DefaultMutableTreeNode, 121 offset: Text.Offset, 122 documents: List[Document_Structure.Document]) 123 { 124 (offset /: documents) { case (i, document) => 125 document match { 126 case Document_Structure.Block(name, text, body) => 127 val range = Text.Range(i, i + document.length) 128 val node = 129 new DefaultMutableTreeNode( 130 new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) 131 parent.add(node) 132 make_tree(node, i, body) 133 case _ => 134 } 135 i + document.length 136 } 137 } 138 139 node_name(buffer) match { 140 case Some(name) => 141 make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer))) 142 true 143 case None => 144 false 145 } 146 } 147} 148 149class Isabelle_Sidekick_Default extends 150 Isabelle_Sidekick_Structure("isabelle", 151 PIDE.resources.theory_node_name, Document_Structure.parse_sections _) 152 153class Isabelle_Sidekick_Context extends 154 Isabelle_Sidekick_Structure("isabelle-context", 155 PIDE.resources.theory_node_name, Document_Structure.parse_blocks _) 156 157class Isabelle_Sidekick_Options extends 158 Isabelle_Sidekick_Structure("isabelle-options", 159 _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _) 160 161class Isabelle_Sidekick_Root extends 162 Isabelle_Sidekick_Structure("isabelle-root", 163 _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _) 164 165class Isabelle_Sidekick_ML extends 166 Isabelle_Sidekick_Structure("isabelle-ml", 167 buffer => Some(PIDE.resources.node_name(buffer)), 168 (_, _, text) => Document_Structure.parse_ml_sections(false, text)) 169 170class Isabelle_Sidekick_SML extends 171 Isabelle_Sidekick_Structure("isabelle-sml", 172 buffer => Some(PIDE.resources.node_name(buffer)), 173 (_, _, text) => Document_Structure.parse_ml_sections(true, text)) 174 175 176class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") 177{ 178 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = 179 { 180 val opt_snapshot = 181 Document_Model.get(buffer) match { 182 case Some(model) if model.is_theory => Some(model.snapshot) 183 case _ => None 184 } 185 opt_snapshot match { 186 case Some(snapshot) => 187 for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) { 188 val markup = 189 snapshot.state.command_markup( 190 snapshot.version, command, Command.Markup_Index.markup, 191 command.range, Markup.Elements.full) 192 Isabelle_Sidekick.swing_markup_tree(markup, data.root, 193 (info: Text.Info[List[XML.Elem]]) => 194 { 195 val range = info.range + command_start 196 val content = command.source(info.range).replace('\n', ' ') 197 val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString 198 199 new DefaultMutableTreeNode( 200 new Isabelle_Sidekick.Asset(command.toString, range) { 201 override def getShortString: String = content 202 override def getLongString: String = info_text 203 override def toString: String = quote(content) + " " + range.toString 204 }) 205 }) 206 } 207 true 208 case None => false 209 } 210 } 211} 212 213 214class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news") 215{ 216 private val Heading1 = """^New in (.*)\w*$""".r 217 private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r 218 219 private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = 220 new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop))) 221 222 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = 223 { 224 var offset = 0 225 var end_offset = 0 226 227 var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None 228 var start2: Option[(Int, String)] = None 229 230 def close1: Unit = 231 start1 match { 232 case Some((start_offset, s, body)) => 233 val node = make_node(s, start_offset, end_offset) 234 body.foreach(node.add(_)) 235 data.root.add(node) 236 start1 = None 237 case None => 238 } 239 240 def close2: Unit = 241 start2 match { 242 case Some((start_offset, s)) => 243 start1 match { 244 case Some((start_offset1, s1, body)) => 245 val node = make_node(s, start_offset, end_offset) 246 start1 = Some((start_offset1, s1, body :+ node)) 247 case None => 248 } 249 start2 = None 250 case None => 251 } 252 253 for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) { 254 line match { 255 case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector())) 256 case Heading2(s) => close2; start2 = Some((offset, s)) 257 case _ => 258 } 259 offset += line.length + 1 260 if (!line.forall(Character.isSpaceChar(_))) end_offset = offset 261 } 262 if (!stopped) { close2; close1 } 263 264 true 265 } 266} 267 268