author | wenzelm |
Fri, 27 Nov 2020 14:25:39 +0100 | |
changeset 72743 | bc82fc605424 |
parent 72742 | bda424c5819f |
child 72744 | 0017eb17ac1c |
permissions | -rw-r--r-- |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/PIDE/command_span.scala |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
3 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
4 |
Syntactic representation of command spans. |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
6 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
8 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
9 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
10 |
import scala.collection.mutable |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
11 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
12 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
13 |
object Command_Span |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
14 |
{ |
72743 | 15 |
/* loaded files */ |
16 |
||
17 |
type Loaded_Files = (List[String], Int) |
|
18 |
||
19 |
val no_loaded_files: Loaded_Files = (Nil, -1) |
|
20 |
||
21 |
def loaded_files(exts: List[String], tokens: List[(Token, Int)]): Loaded_Files = |
|
22 |
tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match { |
|
23 |
case Some((file, i)) => |
|
24 |
if (exts.isEmpty) (List(file), i) |
|
25 |
else (exts.map(ext => file + "." + ext), i) |
|
26 |
case None => no_loaded_files |
|
27 |
} |
|
28 |
||
29 |
||
30 |
/* span kind */ |
|
31 |
||
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
32 |
sealed abstract class Kind { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
33 |
override def toString: String = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
34 |
this match { |
65717 | 35 |
case Command_Span(name, _) => proper_string(name) getOrElse "<command>" |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
36 |
case Ignored_Span => "<ignored>" |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
37 |
case Malformed_Span => "<malformed>" |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
38 |
case Theory_Span => "<theory>" |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
39 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
40 |
} |
57910 | 41 |
case class Command_Span(name: String, pos: Position.T) extends Kind |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
42 |
case object Ignored_Span extends Kind |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
43 |
case object Malformed_Span extends Kind |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
44 |
case object Theory_Span extends Kind |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
45 |
|
72743 | 46 |
|
47 |
/* span */ |
|
48 |
||
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
49 |
sealed case class Span(kind: Kind, content: List[Token]) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
50 |
{ |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
51 |
def is_theory: Boolean = kind == Theory_Span |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
52 |
|
59735 | 53 |
def name: String = |
54 |
kind match { case Command_Span(name, _) => name case _ => "" } |
|
58802 | 55 |
|
59735 | 56 |
def position: Position.T = |
57 |
kind match { case Command_Span(_, pos) => pos case _ => Position.none } |
|
58 |
||
67895 | 59 |
def keyword_pos(start: Token.Pos): Token.Pos = |
60 |
kind match { |
|
61 |
case _: Command_Span => |
|
62 |
(start /: content.iterator.takeWhile(tok => !tok.is_command))(_.advance(_)) |
|
63 |
case _ => start |
|
64 |
} |
|
65 |
||
68845
3b2daa7bf9f4
support Thy_Element in Scala, following ML version;
wenzelm
parents:
68840
diff
changeset
|
66 |
def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean = |
68840 | 67 |
keywords.kinds.get(name) match { |
68 |
case Some(k) => pred(k) |
|
68845
3b2daa7bf9f4
support Thy_Element in Scala, following ML version;
wenzelm
parents:
68840
diff
changeset
|
69 |
case None => other |
68840 | 70 |
} |
71 |
||
63606 | 72 |
def is_begin: Boolean = content.exists(_.is_begin) |
73 |
def is_end: Boolean = content.exists(_.is_end) |
|
74 |
||
59735 | 75 |
def length: Int = (0 /: content)(_ + _.source.length) |
59705 | 76 |
|
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
77 |
def compact_source: (String, Span) = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
78 |
{ |
59735 | 79 |
val source = Token.implode(content) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
80 |
val content1 = new mutable.ListBuffer[Token] |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
81 |
var i = 0 |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
82 |
for (Token(kind, s) <- content) { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
83 |
val n = s.length |
59735 | 84 |
val s1 = source.substring(i, i + n) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
85 |
content1 += Token(kind, s1) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
86 |
i += n |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
87 |
} |
59735 | 88 |
(source, Span(kind, content1.toList)) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
89 |
} |
72742 | 90 |
|
72743 | 91 |
def clean_arguments: List[(Token, Int)] = |
92 |
{ |
|
93 |
if (name.nonEmpty) { |
|
94 |
def clean(toks: List[(Token, Int)]): List[(Token, Int)] = |
|
95 |
toks match { |
|
96 |
case (t1, i1) :: (t2, i2) :: rest => |
|
97 |
if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest) |
|
98 |
else (t1, i1) :: clean((t2, i2) :: rest) |
|
99 |
case _ => toks |
|
100 |
} |
|
101 |
clean(content.zipWithIndex.filter({ case (t, _) => t.is_proper })) |
|
102 |
.dropWhile({ case (t, _) => !t.is_command }) |
|
103 |
.dropWhile({ case (t, _) => t.is_command }) |
|
104 |
} |
|
105 |
else Nil |
|
106 |
} |
|
107 |
||
108 |
def loaded_files(syntax: Outer_Syntax): Loaded_Files = |
|
72742 | 109 |
syntax.load_command(name) match { |
72743 | 110 |
case Some(exts) => isabelle.Command_Span.loaded_files(exts, clean_arguments) |
111 |
case None => no_loaded_files |
|
72742 | 112 |
} |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
113 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
114 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
115 |
val empty: Span = Span(Ignored_Span, Nil) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
116 |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
117 |
def unparsed(source: String, theory: Boolean): Span = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
118 |
{ |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
119 |
val kind = if (theory) Theory_Span else Malformed_Span |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
120 |
Span(kind, List(Token(Token.Kind.UNPARSED, source))) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
121 |
} |
65335 | 122 |
|
123 |
||
124 |
/* XML data representation */ |
|
125 |
||
126 |
def encode: XML.Encode.T[Span] = (span: Span) => |
|
127 |
{ |
|
128 |
import XML.Encode._ |
|
129 |
val kind: T[Kind] = |
|
130 |
variant(List( |
|
131 |
{ case Command_Span(a, b) => (List(a), properties(b)) }, |
|
132 |
{ case Ignored_Span => (Nil, Nil) }, |
|
133 |
{ case Malformed_Span => (Nil, Nil) })) |
|
134 |
pair(kind, list(Token.encode))((span.kind, span.content)) |
|
135 |
} |
|
136 |
||
137 |
def decode: XML.Decode.T[Span] = (body: XML.Body) => |
|
138 |
{ |
|
139 |
import XML.Decode._ |
|
140 |
val kind: T[Kind] = |
|
141 |
variant(List( |
|
142 |
{ case (List(a), b) => Command_Span(a, properties(b)) }, |
|
143 |
{ case (Nil, Nil) => Ignored_Span }, |
|
144 |
{ case (Nil, Nil) => Malformed_Span })) |
|
145 |
val (k, toks) = pair(kind, list(Token.decode))(body) |
|
146 |
Span(k, toks) |
|
147 |
} |
|
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
148 |
} |