author | wenzelm |
Mon, 26 Dec 2016 15:31:13 +0100 | |
changeset 64673 | b5965890e54d |
parent 64672 | d8e0619abb60 |
child 64679 | b2bf280b7e13 |
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 |
||
12 |
import scala.util.parsing.input.CharSequenceReader |
|
13 |
||
14 |
||
15 |
case class Document_Model( |
|
16 |
session: Session, doc: Line.Document, node_name: Document.Node.Name, |
|
17 |
changed: Boolean = true) |
|
18 |
{ |
|
19 |
/* header */ |
|
20 |
||
21 |
def is_theory: Boolean = node_name.is_theory |
|
22 |
||
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
23 |
def node_header(resources: VSCode_Resources): Document.Node.Header = |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
24 |
resources.special_header(node_name) getOrElse |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
25 |
{ |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
26 |
if (is_theory) |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
27 |
session.resources.check_thy_reader( |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
28 |
"", 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
|
29 |
else Document.Node.no_header |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
30 |
} |
64605 | 31 |
|
32 |
||
33 |
/* edits */ |
|
34 |
||
35 |
def text_edits: List[Text.Edit] = |
|
64672 | 36 |
if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil |
64605 | 37 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
38 |
def node_edits(resources: VSCode_Resources): List[Document.Edit_Text] = |
64605 | 39 |
if (changed) { |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
40 |
List(session.header_edit(node_name, node_header(resources)), |
64605 | 41 |
node_name -> Document.Node.Clear(), |
42 |
node_name -> Document.Node.Edits(text_edits), |
|
43 |
node_name -> |
|
44 |
Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)) |
|
45 |
} |
|
46 |
else Nil |
|
47 |
||
48 |
def unchanged: Document_Model = if (changed) copy(changed = false) else this |
|
49 |
||
50 |
||
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
51 |
/* snapshot and rendering */ |
64605 | 52 |
|
53 |
def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits) |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
54 |
|
64667 | 55 |
def rendering(options: Options, text_length: Length): VSCode_Rendering = |
56 |
new VSCode_Rendering(this, snapshot(), options, text_length, session.resources) |
|
64605 | 57 |
} |