equal
deleted
inserted
replaced
47 process_indicator.update(null, 0) |
47 process_indicator.update(null, 0) |
48 } |
48 } |
49 } |
49 } |
50 |
50 |
51 private val sledgehammer = |
51 private val sledgehammer = |
52 new Query_Operation(JEdit_Editor, view, "sledgehammer", consume_status _, |
52 new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _, |
53 (snapshot, results, body) => |
53 (snapshot, results, body) => |
54 pretty_text_area.update(snapshot, results, Pretty.separate(body))) |
54 pretty_text_area.update(snapshot, results, Pretty.separate(body))) |
55 |
55 |
56 |
56 |
57 /* resize */ |
57 /* resize */ |