author  wenzelm 
Fri, 07 May 2010 23:44:10 +0200  
changeset 36738  dce592144219 
parent 36737  17fe629da595 
child 36759  dc972354d77c 
permissions  rwrr 
34393  1 
/* 
36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

2 
* SideKick parsers for Isabelle proof documents 
34393  3 
* 
34407  4 
* @author Fabian Immler, TU Munich 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

5 
* @author Makarius 
34393  6 
*/ 
7 

34426
81f93e0f13b4
renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
wenzelm
parents:
34417
diff
changeset

8 
package isabelle.jedit 
34393  9 

34760  10 

36015  11 
import isabelle._ 
12 

34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset

13 
import scala.collection.Set 
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset

14 
import scala.collection.immutable.TreeSet 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

15 

34393  16 
import javax.swing.tree.DefaultMutableTreeNode 
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset

17 
import javax.swing.text.Position 
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset

18 
import javax.swing.Icon 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

19 

34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset

20 
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

21 
import errorlist.DefaultErrorSource 
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset

22 
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} 
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset

23 

34393  24 

36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

25 
object Isabelle_Sidekick 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

26 
{ 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

27 
implicit def int_to_pos(offset: Int): Position = 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

28 
new Position { def getOffset = offset; override def toString = offset.toString } 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

29 
} 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

30 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

31 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

32 
class Isabelle_Sidekick(name: String, 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

33 
parser: (() => Boolean, SideKickParsedData, Document_Model) => Unit) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

34 
extends SideKickParser(name) 
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset

35 
{ 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

36 
/* parsing */ 
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

37 

34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset

38 
@volatile private var stopped = false 
36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

39 
private def is_stopped(): Boolean = stopped 
34503  40 
override def stop() = { stopped = true } 
34401
44241a37b74a
structure of markuptree in scala, keep track of swingnodes in background
immler@in.tum.de
parents:
34393
diff
changeset

41 

34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset

42 
def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = 
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset

43 
{ 
36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

44 
import Isabelle_Sidekick.int_to_pos 
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34705
diff
changeset

45 

34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

46 
stopped = false 
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset

47 

34789  48 
// FIXME lock buffer !?? 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

49 
val data = new SideKickParsedData(buffer.getName) 
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34705
diff
changeset

50 
val root = data.root 
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34705
diff
changeset

51 
data.getAsset(root).setEnd(buffer.getLength) 
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset

52 

34789  53 
Swing_Thread.now { Document_Model(buffer) } match { 
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset

54 
case Some(model) => 
36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

55 
parser(is_stopped, data, model) 
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset

56 
if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>")) 
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset

57 
case None => root.add(new DefaultMutableTreeNode("<buffer inactive>")) 
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset

58 
} 
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

59 
data 
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

60 
} 
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

61 

36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

62 

34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

63 
/* completion */ 
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

64 

bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

65 
override def supportsCompletion = true 
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

66 
override def canCompleteAnywhere = true 
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser 
wenzelm
parents:
34408
diff
changeset

67 

34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset

68 
override def complete(pane: EditPane, caret: Int): SideKickCompletion = 
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset

69 
{ 
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset

70 
val buffer = pane.getBuffer 
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

71 

5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

72 
val line = buffer.getLineOfOffset(caret) 
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

73 
val start = buffer.getLineStartOffset(line) 
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

74 
val text = buffer.getSegment(start, caret  start) 
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset

75 

34819  76 
val completion = Isabelle.session.current_syntax.completion 
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset

77 

34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

78 
completion.complete(text) match { 
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

79 
case None => null 
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset

80 
case Some((word, cs)) => 
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset

81 
val ds = 
35004
b89a31957950
filter out identical completions only after symbols.decode  recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset

82 
(if (Isabelle_Encoding.is_active(buffer)) 
34796  83 
cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _) 
35004
b89a31957950
filter out identical completions only after symbols.decode  recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset

84 
else cs).filter(_ != word) 
b89a31957950
filter out identical completions only after symbols.decode  recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset

85 
if (ds.isEmpty) null 
b89a31957950
filter out identical completions only after symbols.decode  recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset

86 
else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } 
34611  87 
} 
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset

88 
} 
34393  89 
} 
36738
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

90 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

91 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

92 
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle", 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

93 
((is_stopped: () => Boolean, data: SideKickParsedData, model: Document_Model) => 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

94 
{ 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

95 
import Isabelle_Sidekick.int_to_pos 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

96 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

97 
val root = data.root 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

98 
val document = model.recent_document() 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

99 
for { 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

100 
(command, command_start) < document.command_range(0) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

101 
if command.is_command && !is_stopped() 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

102 
} 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

103 
{ 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

104 
val name = command.name 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

105 
val node = 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

106 
new DefaultMutableTreeNode(new IAsset { 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

107 
override def getIcon: Icon = null 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

108 
override def getShortString: String = name 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

109 
override def getLongString: String = name 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

110 
override def getName: String = name 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

111 
override def setName(name: String) = () 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

112 
override def setStart(start: Position) = () 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

113 
override def getStart: Position = command_start 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

114 
override def setEnd(end: Position) = () 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

115 
override def getEnd: Position = command_start + command.length 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

116 
override def toString = name 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

117 
}) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

118 
root.add(node) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

119 
} 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

120 
})) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

121 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

122 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

123 
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelleraw", 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

124 
((is_stopped: () => Boolean, data: SideKickParsedData, model: Document_Model) => 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

125 
{ 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

126 
import Isabelle_Sidekick.int_to_pos 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

127 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

128 
val root = data.root 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

129 
val document = model.recent_document() 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

130 
for ((command, command_start) < document.command_range(0) if !is_stopped()) { 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

131 
root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) => 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

132 
{ 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

133 
val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop)))) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

134 
val id = command.id 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

135 

dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

136 
new DefaultMutableTreeNode(new IAsset { 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

137 
override def getIcon: Icon = null 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

138 
override def getShortString: String = content 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

139 
override def getLongString: String = node.info.toString 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

140 
override def getName: String = id 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

141 
override def setName(name: String) = () 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

142 
override def setStart(start: Position) = () 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

143 
override def getStart: Position = command_start + node.start 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

144 
override def setEnd(end: Position) = () 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

145 
override def getEnd: Position = command_start + node.stop 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

146 
override def toString = id + ": " + content + "[" + getStart + "  " + getEnd + "]" 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

147 
}) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

148 
})) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

149 
} 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

150 
})) 
dce592144219
support several sidekick parsers  very basic default parser;
wenzelm
parents:
36737
diff
changeset

151 