author | wenzelm |
Sat, 07 Jan 2017 20:44:37 +0100 | |
changeset 64826 | c97296294f6d |
parent 64824 | 330ec9bc4b75 |
child 64827 | 4ef1eb75f1cd |
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 |
|
64707 | 15 |
object Document_Model |
16 |
{ |
|
64777
ca09695eb43c
clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents:
64775
diff
changeset
|
17 |
def init(session: Session, node_name: Document.Node.Name): Document_Model = |
64707 | 18 |
{ |
19 |
val resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64709 | 20 |
val doc = Line.Document("", resources.text_length) |
21 |
Document_Model(session, node_name, doc) |
|
64707 | 22 |
} |
23 |
} |
|
24 |
||
64710 | 25 |
sealed case class Document_Model( |
64707 | 26 |
session: Session, |
27 |
node_name: Document.Node.Name, |
|
28 |
doc: Line.Document, |
|
64726 | 29 |
external_file: Boolean = false, |
64707 | 30 |
node_required: Boolean = false, |
31 |
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, |
|
64816 | 32 |
pending_edits: List[Text.Edit] = Nil, |
64814 | 33 |
published_diagnostics: List[Text.Info[Command.Results]] = Nil) extends Document.Model |
64605 | 34 |
{ |
64710 | 35 |
/* external file */ |
36 |
||
64727
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
37 |
def external(b: Boolean): Document_Model = copy(external_file = b) |
13e37567a0d6
automatically resolve dependencies from document models and file-system;
wenzelm
parents:
64726
diff
changeset
|
38 |
|
64800 | 39 |
def node_visible: Boolean = !external_file |
40 |
||
64710 | 41 |
|
64690 | 42 |
/* header */ |
43 |
||
64702 | 44 |
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
|
45 |
resources.special_header(node_name) getOrElse |
64826
c97296294f6d
clarified check_thy_reader: check node_name here;
wenzelm
parents:
64824
diff
changeset
|
46 |
resources.check_thy_reader("", node_name, Scan.char_reader(doc.text)) |
64605 | 47 |
|
48 |
||
64707 | 49 |
/* perspective */ |
50 |
||
64800 | 51 |
def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |
52 |
{ |
|
53 |
if (is_theory) { |
|
54 |
val snapshot = this.snapshot() |
|
55 |
||
56 |
val text_perspective = |
|
57 |
if (node_visible || snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) |
|
58 |
Text.Perspective.full |
|
59 |
else Text.Perspective.empty |
|
64723 | 60 |
|
64800 | 61 |
(snapshot.node.load_commands_changed(doc_blobs), |
62 |
Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)) |
|
63 |
} |
|
64 |
else (false, Document.Node.no_perspective_text) |
|
65 |
} |
|
66 |
||
64707 | 67 |
|
64800 | 68 |
/* blob */ |
69 |
||
70 |
def get_blob: Option[Document.Blob] = |
|
71 |
if (is_theory) None |
|
64821 | 72 |
else Some((Document.Blob(doc.bytes, doc.chunk, pending_edits.nonEmpty))) |
64707 | 73 |
|
74 |
||
64605 | 75 |
/* edits */ |
76 |
||
64806 | 77 |
def update_text(text: String): Option[Document_Model] = |
64709 | 78 |
{ |
64821 | 79 |
val old_text = doc.text |
64806 | 80 |
val new_text = Line.normalize(text) |
64816 | 81 |
Text.Edit.replace(0, old_text, new_text) match { |
82 |
case Nil => None |
|
83 |
case edits => |
|
84 |
val doc1 = Line.Document(new_text, doc.text_length) |
|
85 |
val pending_edits1 = pending_edits ::: edits |
|
86 |
Some(copy(doc = doc1, pending_edits = pending_edits1)) |
|
64709 | 87 |
} |
88 |
} |
|
89 |
||
64800 | 90 |
def flush_edits(doc_blobs: Document.Blobs): Option[(List[Document.Edit_Text], Document_Model)] = |
64707 | 91 |
{ |
64800 | 92 |
val (reparse, perspective) = node_perspective(doc_blobs) |
93 |
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { |
|
94 |
val edits: List[Document.Edit_Text] = |
|
95 |
get_blob match { |
|
96 |
case None => |
|
97 |
List(session.header_edit(node_name, node_header), |
|
64816 | 98 |
node_name -> Document.Node.Edits(pending_edits), |
64800 | 99 |
node_name -> perspective) |
100 |
case Some(blob) => |
|
101 |
List(node_name -> Document.Node.Blob(blob), |
|
64816 | 102 |
node_name -> Document.Node.Edits(pending_edits)) |
64800 | 103 |
} |
64816 | 104 |
Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) |
64605 | 105 |
} |
64707 | 106 |
else None |
107 |
} |
|
64605 | 108 |
|
109 |
||
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
110 |
/* diagnostics */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
111 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
112 |
def publish_diagnostics(rendering: VSCode_Rendering) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
113 |
: Option[(List[Text.Info[Command.Results]], Document_Model)] = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
114 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
115 |
val diagnostics = rendering.diagnostics |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
116 |
if (diagnostics == published_diagnostics) None |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
117 |
else Some(diagnostics, copy(published_diagnostics = diagnostics)) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
118 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
119 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
120 |
|
64725 | 121 |
/* prover session */ |
64702 | 122 |
|
123 |
def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] |
|
64605 | 124 |
|
64816 | 125 |
def is_stable: Boolean = pending_edits.isEmpty |
126 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
127 |
|
64704 | 128 |
def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources) |
64605 | 129 |
} |