author | wenzelm |
Sat, 31 Dec 2016 15:31:56 +0100 | |
changeset 64725 | 38305f56c769 |
parent 64723 | 65bcb1fbaa73 |
child 64726 | c534a2ac537d |
permissions | -rw-r--r-- |
64605 | 1 |
/* Title: Tools/VSCode/src/document_model.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Document model for line-oriented text. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.vscode |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
64710 | 12 |
import java.io.{File => JFile} |
13 |
||
64605 | 14 |
import scala.util.parsing.input.CharSequenceReader |
15 |
||
16 |
||
64707 | 17 |
object Document_Model |
18 |
{ |
|
64709 | 19 |
def init(session: Session, uri: String): Document_Model = |
64707 | 20 |
{ |
21 |
val resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64709 | 22 |
val node_name = resources.node_name(uri) |
23 |
val doc = Line.Document("", resources.text_length) |
|
24 |
Document_Model(session, node_name, doc) |
|
64707 | 25 |
} |
26 |
} |
|
27 |
||
64710 | 28 |
sealed case class Document_Model( |
64707 | 29 |
session: Session, |
30 |
node_name: Document.Node.Name, |
|
31 |
doc: Line.Document, |
|
64710 | 32 |
external: Boolean = false, |
64707 | 33 |
node_required: Boolean = false, |
34 |
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
|
64709 | 35 |
pending_edits: Vector[Text.Edit] = Vector.empty, |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
36 |
published_diagnostics: List[Text.Info[Command.Results]] = Nil) |
64605 | 37 |
{ |
64702 | 38 |
/* name */ |
64680 | 39 |
|
64702 | 40 |
override def toString: String = node_name.toString |
64605 | 41 |
|
64690 | 42 |
def uri: String = node_name.node |
64605 | 43 |
def is_theory: Boolean = node_name.is_theory |
44 |
||
64690 | 45 |
|
64710 | 46 |
/* external file */ |
47 |
||
48 |
val file: JFile = VSCode_Resources.canonical_file(uri) |
|
49 |
||
50 |
def register(watcher: File_Watcher) |
|
51 |
{ |
|
52 |
val dir = file.getParentFile |
|
53 |
if (dir != null && dir.isDirectory) watcher.register(dir) |
|
54 |
} |
|
55 |
||
56 |
||
64690 | 57 |
/* header */ |
58 |
||
64702 | 59 |
def node_header: Document.Node.Header = |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
60 |
resources.special_header(node_name) getOrElse |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
61 |
{ |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
62 |
if (is_theory) |
64702 | 63 |
resources.check_thy_reader( |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
64 |
"", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command) |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
65 |
else Document.Node.no_header |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
66 |
} |
64605 | 67 |
|
68 |
||
64707 | 69 |
/* perspective */ |
70 |
||
64723 | 71 |
def node_visible: Boolean = !external |
72 |
||
64707 | 73 |
def text_perspective: Text.Perspective = |
74 |
if (node_visible) Text.Perspective.full else Text.Perspective.empty |
|
75 |
||
76 |
def node_perspective: Document.Node.Perspective_Text = |
|
77 |
Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty) |
|
78 |
||
79 |
||
64605 | 80 |
/* edits */ |
81 |
||
64710 | 82 |
def update_text(new_text: String): Option[Document_Model] = |
64709 | 83 |
{ |
84 |
val old_text = doc.make_text |
|
64710 | 85 |
if (new_text == old_text) None |
64709 | 86 |
else { |
87 |
val doc1 = Line.Document(new_text, doc.text_length) |
|
88 |
val pending_edits1 = |
|
89 |
if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits |
|
90 |
val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text) |
|
64710 | 91 |
Some(copy(doc = doc1, pending_edits = pending_edits2)) |
64709 | 92 |
} |
93 |
} |
|
94 |
||
64710 | 95 |
def update_file: Option[Document_Model] = |
96 |
if (external) { |
|
97 |
try { update_text(File.read(file)) } |
|
98 |
catch { case ERROR(_) => None } |
|
99 |
} |
|
100 |
else None |
|
101 |
||
64707 | 102 |
def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] = |
103 |
{ |
|
104 |
val perspective = node_perspective |
|
64709 | 105 |
if (pending_edits.nonEmpty || last_perspective != perspective) { |
106 |
val text_edits = pending_edits.toList |
|
107 |
val edits = |
|
108 |
session.header_edit(node_name, node_header) :: |
|
109 |
(if (text_edits.isEmpty) Nil |
|
110 |
else List[Document.Edit_Text](node_name -> Document.Node.Edits(text_edits))) ::: |
|
111 |
(if (last_perspective == perspective) Nil |
|
112 |
else List[Document.Edit_Text](node_name -> perspective)) |
|
113 |
Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective))) |
|
64605 | 114 |
} |
64707 | 115 |
else None |
116 |
} |
|
64605 | 117 |
|
118 |
||
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
119 |
/* diagnostics */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
120 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
121 |
def publish_diagnostics(rendering: VSCode_Rendering) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
122 |
: Option[(List[Text.Info[Command.Results]], Document_Model)] = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
123 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
124 |
val diagnostics = rendering.diagnostics |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
125 |
if (diagnostics == published_diagnostics) None |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
126 |
else Some(diagnostics, copy(published_diagnostics = diagnostics)) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
127 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
128 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
129 |
|
64725 | 130 |
/* prover session */ |
64702 | 131 |
|
132 |
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64605 | 133 |
|
64709 | 134 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList) |
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
135 |
|
64704 | 136 |
def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources) |
64605 | 137 |
} |