src/Tools/jEdit/src/isabelle_sidekick.scala
changeset 46208 4cab63a6dc16
parent 46194 872f915e3a98
child 46920 5f44c8bea84e
equal deleted inserted replaced
46207:e76b77356ed6 46208:4cab63a6dc16
   150   def parser(data: SideKickParsedData, model: Document_Model)
   150   def parser(data: SideKickParsedData, model: Document_Model)
   151   {
   151   {
   152     val root = data.root
   152     val root = data.root
   153     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   153     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   154     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   154     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   155       snapshot.command_state(command).markup.swing_tree(root)((info: Text.Markup) =>
   155       snapshot.state.command_state(snapshot.version, command).markup
       
   156         .swing_tree(root)((info: Text.Markup) =>
   156           {
   157           {
   157             val range = info.range + command_start
   158             val range = info.range + command_start
   158             val content = command.source(info.range).replace('\n', ' ')
   159             val content = command.source(info.range).replace('\n', ' ')
   159             val info_text =
   160             val info_text =
   160               info.info match {
   161               info.info match {