author | wenzelm |
Sat, 10 Dec 2022 21:02:09 +0100 | |
changeset 76615 | b865959e2547 |
parent 75393 | 87ebf5a50283 |
child 76798 | 69d8d16c5612 |
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 |
72946 | 11 |
import scala.util.parsing.input.CharSequenceReader |
57905
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 |
|
75393 | 14 |
object Command_Span { |
72743 | 15 |
/* loaded files */ |
16 |
||
75393 | 17 |
object Loaded_Files { |
72757 | 18 |
val none: Loaded_Files = Loaded_Files(Nil, -1) |
19 |
} |
|
20 |
sealed case class Loaded_Files(files: List[String], index: Int) |
|
72743 | 21 |
|
74671 | 22 |
abstract class Load_Command(val name: String, val here: Scala_Project.Here) |
75393 | 23 |
extends Isabelle_System.Service { |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
24 |
override def toString: String = name |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
25 |
|
74671 | 26 |
def position: Position.T = here.position |
27 |
||
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
28 |
def extensions: List[String] = Nil |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
29 |
|
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
30 |
def loaded_files(tokens: List[(Token, Int)]): Loaded_Files = |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
31 |
tokens.collectFirst({ case (t, i) if t.is_embedded => (t.content, i) }) match { |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
32 |
case Some((file, i)) => |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
33 |
extensions match { |
72757 | 34 |
case Nil => Loaded_Files(List(file), i) |
35 |
case exts => Loaded_Files(exts.map(ext => file + "." + ext), i) |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
36 |
} |
72757 | 37 |
case None => Loaded_Files.none |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
38 |
} |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
39 |
} |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
40 |
|
76615 | 41 |
object Load_Default extends Load_Command("", Scala_Project.here) |
74671 | 42 |
|
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
43 |
lazy val load_commands: List[Load_Command] = |
76615 | 44 |
Load_Default :: Isabelle_System.make_services(classOf[Load_Command]) |
72743 | 45 |
|
46 |
||
47 |
/* span kind */ |
|
48 |
||
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
49 |
sealed abstract class Kind { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
50 |
override def toString: String = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
51 |
this match { |
73115
a8e5d7c9a834
discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;
wenzelm
parents:
72946
diff
changeset
|
52 |
case Command_Span(name, _) => proper_string(name) getOrElse "<command>" |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
53 |
case Ignored_Span => "<ignored>" |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
54 |
case Malformed_Span => "<malformed>" |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
55 |
case Theory_Span => "<theory>" |
57905
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 |
} |
73115
a8e5d7c9a834
discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;
wenzelm
parents:
72946
diff
changeset
|
58 |
case class Command_Span(name: String, pos: Position.T) extends Kind |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
59 |
case object Ignored_Span extends Kind |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
60 |
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
|
61 |
case object Theory_Span extends Kind |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
62 |
|
72743 | 63 |
|
64 |
/* span */ |
|
65 |
||
75393 | 66 |
sealed case class Span(kind: Kind, content: List[Token]) { |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
67 |
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
|
68 |
|
59735 | 69 |
def name: String = |
72800 | 70 |
kind match { case k: Command_Span => k.name case _ => "" } |
58802 | 71 |
|
59735 | 72 |
def position: Position.T = |
72800 | 73 |
kind match { case k: Command_Span => k.pos case _ => Position.none } |
74 |
||
67895 | 75 |
def keyword_pos(start: Token.Pos): Token.Pos = |
76 |
kind match { |
|
77 |
case _: Command_Span => |
|
73359 | 78 |
content.iterator.takeWhile(tok => !tok.is_command).foldLeft(start)(_.advance(_)) |
67895 | 79 |
case _ => start |
80 |
} |
|
81 |
||
68845
3b2daa7bf9f4
support Thy_Element in Scala, following ML version;
wenzelm
parents:
68840
diff
changeset
|
82 |
def is_kind(keywords: Keyword.Keywords, pred: String => Boolean, other: Boolean): Boolean = |
68840 | 83 |
keywords.kinds.get(name) match { |
84 |
case Some(k) => pred(k) |
|
68845
3b2daa7bf9f4
support Thy_Element in Scala, following ML version;
wenzelm
parents:
68840
diff
changeset
|
85 |
case None => other |
68840 | 86 |
} |
87 |
||
63606 | 88 |
def is_begin: Boolean = content.exists(_.is_begin) |
89 |
def is_end: Boolean = content.exists(_.is_end) |
|
90 |
||
72946 | 91 |
def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content)) |
92 |
||
73359 | 93 |
def length: Int = content.foldLeft(0)(_ + _.source.length) |
59705 | 94 |
|
75393 | 95 |
def compact_source: (String, Span) = { |
59735 | 96 |
val source = Token.implode(content) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
97 |
val content1 = new mutable.ListBuffer[Token] |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
98 |
var i = 0 |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
99 |
for (Token(kind, s) <- content) { |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
100 |
val n = s.length |
59735 | 101 |
val s1 = source.substring(i, i + n) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
102 |
content1 += Token(kind, s1) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
103 |
i += n |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
104 |
} |
59735 | 105 |
(source, Span(kind, content1.toList)) |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
106 |
} |
72742 | 107 |
|
75393 | 108 |
def clean_arguments: List[(Token, Int)] = { |
72743 | 109 |
if (name.nonEmpty) { |
110 |
def clean(toks: List[(Token, Int)]): List[(Token, Int)] = |
|
111 |
toks match { |
|
112 |
case (t1, i1) :: (t2, i2) :: rest => |
|
113 |
if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest) |
|
114 |
else (t1, i1) :: clean((t2, i2) :: rest) |
|
115 |
case _ => toks |
|
116 |
} |
|
117 |
clean(content.zipWithIndex.filter({ case (t, _) => t.is_proper })) |
|
118 |
.dropWhile({ case (t, _) => !t.is_command }) |
|
119 |
.dropWhile({ case (t, _) => t.is_command }) |
|
120 |
} |
|
121 |
else Nil |
|
122 |
} |
|
123 |
||
72816
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72800
diff
changeset
|
124 |
def is_load_command(syntax: Outer_Syntax): Boolean = |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72800
diff
changeset
|
125 |
syntax.load_command(name).isDefined |
ea4f86914cb2
support for PIDE markup for auxiliary files ("blobs");
wenzelm
parents:
72800
diff
changeset
|
126 |
|
72743 | 127 |
def loaded_files(syntax: Outer_Syntax): Loaded_Files = |
72742 | 128 |
syntax.load_command(name) match { |
72757 | 129 |
case None => Loaded_Files.none |
72748
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
130 |
case Some(a) => |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
131 |
load_commands.find(_.name == a) match { |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
132 |
case Some(load_command) => load_command.loaded_files(clean_arguments) |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
133 |
case None => error("Undefined load command function: " + a) |
04d5f6d769a7
more flexible syntax for theory load commands via Isabelle/Scala;
wenzelm
parents:
72744
diff
changeset
|
134 |
} |
72742 | 135 |
} |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
136 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
137 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
138 |
val empty: Span = Span(Ignored_Span, Nil) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
139 |
|
75393 | 140 |
def unparsed(source: String, theory: Boolean): Span = { |
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
68845
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
} |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
diff
changeset
|
144 |
} |