author  wenzelm 
Mon, 10 Dec 2012 13:52:33 +0100  
changeset 50450  358b6020f8b6 
parent 50341  src/Tools/jEdit/src/sendback.scala@0c65a7cfc0f3 
child 50452  bfb5964e3041 
permissions  rwrr 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

1 
/* Title: Tools/jEdit/src/active.scala 
49492  2 
Author: Makarius 
3 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

4 
Active areas within the document. 
49492  5 
*/ 
6 

7 
package isabelle.jedit 

8 

9 

10 
import isabelle._ 

11 

49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset

12 
import org.gjt.sp.jedit.View 
49492  13 

14 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

15 
object Active 
49492  16 
{ 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

17 
def action(view: View, text: String, elem: XML.Elem) 
49492  18 
{ 
19 
Swing_Thread.require() 

20 

21 
Document_View(view.getTextArea) match { 

22 
case Some(doc_view) => 

23 
doc_view.rich_text_area.robust_body() { 

50215  24 
val text_area = doc_view.text_area 
49492  25 
val model = doc_view.model 
26 
val buffer = model.buffer 

27 
val snapshot = model.snapshot() 

49493
db58490a68ac
more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents:
49492
diff
changeset

28 

50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset

29 
if (!snapshot.is_outdated) { 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

30 
elem match { 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

31 
case XML.Elem(Markup(Markup.SENDBACK, props), _) => 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

32 
props match { 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

33 
case Position.Id(exec_id) => 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

34 
snapshot.state.execs.get(exec_id).map(_.command) match { 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

35 
case Some(command) => 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

36 
snapshot.node.command_start(command) match { 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

37 
case Some(start) => 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

38 
JEdit_Lib.buffer_edit(buffer) { 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

39 
buffer.remove(start, command.proper_range.length) 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

40 
buffer.insert(start, text) 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

41 
} 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

42 
case None => 
50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset

43 
} 
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset

44 
case None => 
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset

45 
} 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

46 
case _ => 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

47 
if (props.exists(_ == Markup.PADDING_LINE)) 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

48 
Isabelle.insert_line_padding(text_area, text) 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

49 
else text_area.setSelectedText(text) 
50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset

50 
} 
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

51 

358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

52 
case XML.Elem(Markup(Markup.GRAPHVIEW, props), body) => 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

53 
java.lang.System.err.println("graphview " + props) // FIXME 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50341
diff
changeset

54 

50215  55 
case _ => 
50164
77668b522ffe
some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents:
49493
diff
changeset

56 
} 
49492  57 
} 
58 
} 

59 
case None => 

60 
} 

61 
} 

62 
} 

63 