author | wenzelm |
Fri, 01 Sep 2017 15:15:29 +0200 | |
changeset 66591 | 6efa351190d0 |
parent 66206 | 2d2082db735a |
child 72135 | f67e83608745 |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
39588
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/protocol_dockable.scala |
36760 | 2 |
Author: Makarius |
3 |
||
37067 | 4 |
Dockable window for protocol messages. |
36760 | 5 |
*/ |
34408 | 6 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
36015 | 10 |
import isabelle._ |
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66206
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
36015 | 12 |
|
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
13 |
import java.awt.BorderLayout |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
14 |
|
37067 | 15 |
import scala.swing.{TextArea, ScrollPane} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
16 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.View |
34424 | 18 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
|
37067 | 20 |
class Protocol_Dockable(view: View, position: String) extends Dockable(view, position) |
34760 | 21 |
{ |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
22 |
/* controls */ |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
23 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
24 |
private val ml_stats = new Isabelle.ML_Stats |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
25 |
|
66206 | 26 |
private val controls = Wrap_Panel(List(ml_stats)) |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
27 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
28 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
29 |
/* text area */ |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
30 |
|
37067 | 31 |
private val text_area = new TextArea |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
32 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
33 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
34 |
/* layout */ |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
35 |
|
37067 | 36 |
set_content(new ScrollPane(text_area)) |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
37 |
add(controls.peer, BorderLayout.NORTH) |
34772 | 38 |
|
39 |
||
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56391
diff
changeset
|
40 |
/* main */ |
34671 | 41 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56391
diff
changeset
|
42 |
private val main = |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
43 |
Session.Consumer[Any](getClass.getName) { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56391
diff
changeset
|
44 |
case input: Prover.Input => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
45 |
GUI_Thread.later { text_area.append(input.toString + "\n\n") } |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43520
diff
changeset
|
46 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56391
diff
changeset
|
47 |
case output: Prover.Output => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56715
diff
changeset
|
48 |
GUI_Thread.later { text_area.append(output.message.toString + "\n\n") } |
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
49 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
50 |
case _: Session.Global_Options => |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
51 |
GUI_Thread.later { ml_stats.load() } |
34772 | 52 |
} |
53 |
||
60074
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
54 |
override def init() |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
55 |
{ |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
56 |
PIDE.session.all_messages += main |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
57 |
PIDE.session.global_options += main |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
58 |
} |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
59 |
|
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
60 |
override def exit() |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
61 |
{ |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
62 |
PIDE.session.all_messages -= main |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
63 |
PIDE.session.global_options -= main |
38a64cc17403
GUI controls for ML_statistics, for more digestible protocol dump;
wenzelm
parents:
57612
diff
changeset
|
64 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
65 |
} |