author | wenzelm |
Tue, 21 Oct 2014 17:49:51 +0200 | |
changeset 58749 | 83b0f633190e |
parent 57910 | a50837b637dc |
child 58802 | 3cc68ec558b0 |
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 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
15 |
sealed abstract class Kind { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
16 |
override def toString: String = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
17 |
this match { |
57910 | 18 |
case Command_Span(name, _) => if (name != "") name else "<command>" |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
19 |
case Ignored_Span => "<ignored>" |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
20 |
case Malformed_Span => "<malformed>" |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
21 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
22 |
} |
57910 | 23 |
case class Command_Span(name: String, pos: Position.T) extends Kind |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
24 |
case object Ignored_Span extends Kind |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
25 |
case object Malformed_Span extends Kind |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
26 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
27 |
sealed case class Span(kind: Kind, content: List[Token]) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
28 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
29 |
def compact_source: (String, Span) = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
30 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
31 |
val source: String = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
32 |
content match { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
33 |
case List(tok) => tok.source |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
34 |
case toks => toks.map(_.source).mkString |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
35 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
36 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
37 |
val content1 = new mutable.ListBuffer[Token] |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
38 |
var i = 0 |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
39 |
for (Token(kind, s) <- content) { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
40 |
val n = s.length |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
41 |
val s1 = source.substring(i, i + n) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
42 |
content1 += Token(kind, s1) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
43 |
i += n |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
44 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
45 |
(source, Span(kind, content1.toList)) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
46 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
47 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
48 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
49 |
val empty: Span = Span(Ignored_Span, Nil) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
50 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
51 |
def unparsed(source: String): Span = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
52 |
Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source))) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
53 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
54 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
55 |
/* resolve inlined files */ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
56 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
57 |
private def find_file(tokens: List[Token]): Option[String] = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
58 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
59 |
def clean(toks: List[Token]): List[Token] = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
60 |
toks match { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
61 |
case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
62 |
case t :: ts => t :: clean(ts) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
63 |
case Nil => Nil |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
64 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
65 |
clean(tokens.filter(_.is_proper)) match { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
66 |
case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
67 |
case _ => None |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
68 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
69 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
70 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
71 |
def span_files(syntax: Prover.Syntax, span: Span): List[String] = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
72 |
span.kind match { |
57910 | 73 |
case Command_Span(name, _) => |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
74 |
syntax.load_command(name) match { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
75 |
case Some(exts) => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
76 |
find_file(span.content) match { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
77 |
case Some(file) => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
78 |
if (exts.isEmpty) List(file) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
79 |
else exts.map(ext => file + "." + ext) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
80 |
case None => Nil |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
81 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
82 |
case None => Nil |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
83 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
84 |
case _ => Nil |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
85 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
86 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
87 |
def resolve_files( |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
88 |
resources: Resources, |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
89 |
syntax: Prover.Syntax, |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
90 |
node_name: Document.Node.Name, |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
91 |
span: Span, |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
92 |
get_blob: Document.Node.Name => Option[Document.Blob]) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
93 |
: List[Command.Blob] = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
94 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
95 |
span_files(syntax, span).map(file_name => |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
96 |
Exn.capture { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
97 |
val name = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
98 |
Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name))) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
99 |
val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk))) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
100 |
(name, blob) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
101 |
}) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
102 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
103 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
104 |