equal
deleted
inserted
replaced
28 /* text area */ |
28 /* text area */ |
29 |
29 |
30 val pretty_text_area = new Pretty_Text_Area(view) |
30 val pretty_text_area = new Pretty_Text_Area(view) |
31 set_content(pretty_text_area) |
31 set_content(pretty_text_area) |
32 |
32 |
33 override def detach_operation = pretty_text_area.detach_operation |
33 override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation |
34 |
34 |
35 |
35 |
36 /* query operation */ |
36 /* query operation */ |
37 |
37 |
38 private val process_indicator = new Process_Indicator |
38 private val process_indicator = new Process_Indicator |
48 process_indicator.update(null, 0) |
48 process_indicator.update(null, 0) |
49 } |
49 } |
50 } |
50 } |
51 |
51 |
52 private val sledgehammer = |
52 private val sledgehammer = |
53 new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _, |
53 new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, |
54 (snapshot, results, body) => |
54 (snapshot, results, body) => |
55 pretty_text_area.update(snapshot, results, Pretty.separate(body))) |
55 pretty_text_area.update(snapshot, results, Pretty.separate(body))) |
56 |
56 |
57 |
57 |
58 /* resize */ |
58 /* resize */ |