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