equal
deleted
inserted
replaced
40 |
40 |
41 theory_view = new TheoryView(view.getTextArea, prover) |
41 theory_view = new TheoryView(view.getTextArea, prover) |
42 prover.set_document(theory_view.change_receiver, |
42 prover.set_document(theory_view.change_receiver, |
43 if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) |
43 if (path.startsWith(Isabelle.VFS_PREFIX)) path.substring(Isabelle.VFS_PREFIX.length) else path) |
44 theory_view.activate |
44 theory_view.activate |
45 prover ! new isabelle.proofdocument.Text.Change(Isabelle.plugin.id(), 0,buffer.getText(0, buffer.getLength),0) |
45 val MCL = TheoryView.MAX_CHANGE_LENGTH |
|
46 for (i <- 0 to buffer.getLength / MCL) prover ! |
|
47 new isabelle.proofdocument.Text.Change(Isabelle.plugin.id(), i * MCL, |
|
48 buffer.getText(i * MCL, |
|
49 MCL min buffer.getLength - i * MCL),0) |
46 |
50 |
47 //register output-view |
51 //register output-view |
48 prover.output_info += (text => |
52 prover.output_info += (text => |
49 { |
53 { |
50 output_text_view.append(text + "\n") |
54 output_text_view.append(text + "\n") |