src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
changeset 36990 449628c148cf
parent 36764 17427cf6fe95
child 38150 67fc24df3721
equal deleted inserted replaced
36989:aaa7cac3e54a 36990:449628c148cf
   128     import Isabelle_Sidekick.int_to_pos
   128     import Isabelle_Sidekick.int_to_pos
   129 
   129 
   130     val root = data.root
   130     val root = data.root
   131     val document = model.recent_document()
   131     val document = model.recent_document()
   132     for ((command, command_start) <- document.command_range(0) if !stopped) {
   132     for ((command, command_start) <- document.command_range(0) if !stopped) {
   133       root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) =>
   133       root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
   134           {
   134           {
   135             val content = command.source(node.start, node.stop).replace('\n', ' ')
   135             val content = command.source(node.start, node.stop).replace('\n', ' ')
   136             val id = command.id
   136             val id = command.id
   137 
   137 
   138             new DefaultMutableTreeNode(new IAsset {
   138             new DefaultMutableTreeNode(new IAsset {