equal
deleted
inserted
replaced
77 } |
77 } |
78 |
78 |
79 |
79 |
80 /* overlays */ |
80 /* overlays */ |
81 |
81 |
82 private var overlays = Document.Overlays.empty |
82 private var overlays = Document.Node.Overlays.empty |
83 |
83 |
84 def insert_overlay(command: Command, name: String, args: List[String]): Unit = |
84 def insert_overlay(command: Command, name: String, args: List[String]): Unit = |
85 Swing_Thread.require { overlays = overlays.insert(command, (name, args)) } |
85 Swing_Thread.require { overlays = overlays.insert(command, (name, args)) } |
86 |
86 |
87 def remove_overlay(command: Command, name: String, args: List[String]): Unit = |
87 def remove_overlay(command: Command, name: String, args: List[String]): Unit = |
102 PIDE.flush_buffers() |
102 PIDE.flush_buffers() |
103 } |
103 } |
104 } |
104 } |
105 |
105 |
106 val empty_perspective: Document.Node.Perspective_Text = |
106 val empty_perspective: Document.Node.Perspective_Text = |
107 Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty) |
107 Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty) |
108 |
108 |
109 def node_perspective(): Document.Node.Perspective_Text = |
109 def node_perspective(): Document.Node.Perspective_Text = |
110 { |
110 { |
111 Swing_Thread.require() |
111 Swing_Thread.require() |
112 |
112 |