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