author | wenzelm |
Wed, 28 Dec 2016 16:50:14 +0100 | |
changeset 64680 | 7f87c1aa0ffa |
parent 64679 | b2bf280b7e13 |
child 64682 | 7e119f32276a |
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( |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
16 |
session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
17 |
changed: Boolean = true, |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
18 |
published_diagnostics: List[Text.Info[Command.Results]] = Nil) |
64605 | 19 |
{ |
64680 | 20 |
override def toString: String = node_name.toString |
21 |
||
22 |
||
64605 | 23 |
/* header */ |
24 |
||
25 |
def is_theory: Boolean = node_name.is_theory |
|
26 |
||
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
27 |
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
|
28 |
resources.special_header(node_name) getOrElse |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
29 |
{ |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
30 |
if (is_theory) |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
31 |
session.resources.check_thy_reader( |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
32 |
"", 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
|
33 |
else Document.Node.no_header |
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
34 |
} |
64605 | 35 |
|
36 |
||
37 |
/* edits */ |
|
38 |
||
39 |
def text_edits: List[Text.Edit] = |
|
64672 | 40 |
if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil |
64605 | 41 |
|
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
42 |
def node_edits(resources: VSCode_Resources): List[Document.Edit_Text] = |
64605 | 43 |
if (changed) { |
64673
b5965890e54d
more uniform treatment of file name vs. theory name and special header;
wenzelm
parents:
64672
diff
changeset
|
44 |
List(session.header_edit(node_name, node_header(resources)), |
64605 | 45 |
node_name -> Document.Node.Clear(), |
46 |
node_name -> Document.Node.Edits(text_edits), |
|
47 |
node_name -> |
|
48 |
Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)) |
|
49 |
} |
|
50 |
else Nil |
|
51 |
||
52 |
def unchanged: Document_Model = if (changed) copy(changed = false) else this |
|
53 |
||
54 |
||
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
55 |
/* diagnostics */ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
56 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
57 |
def publish_diagnostics(rendering: VSCode_Rendering) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
58 |
: Option[(List[Text.Info[Command.Results]], Document_Model)] = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
59 |
{ |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
60 |
val diagnostics = rendering.diagnostics |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
61 |
if (diagnostics == published_diagnostics) None |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
62 |
else Some(diagnostics, copy(published_diagnostics = diagnostics)) |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
63 |
} |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
64 |
|
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
65 |
|
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
64605
diff
changeset
|
66 |
/* snapshot and rendering */ |
64605 | 67 |
|
68 |
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
|
69 |
|
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
70 |
def rendering(options: Options): VSCode_Rendering = |
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64673
diff
changeset
|
71 |
new VSCode_Rendering(this, snapshot(), options, session.resources) |
64605 | 72 |
} |