author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 70148 | 73a34cb9e67e |
child 71165 | 03afc8252225 |
permissions | -rw-r--r-- |
63604 | 1 |
/* Title: Pure/Isar/document_structure.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Overall document structure. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import scala.collection.mutable |
|
11 |
import scala.annotation.tailrec |
|
12 |
||
13 |
||
14 |
object Document_Structure |
|
15 |
{ |
|
63610 | 16 |
/** general structure **/ |
63604 | 17 |
|
18 |
sealed abstract class Document { def length: Int } |
|
19 |
case class Block(name: String, text: String, body: List[Document]) extends Document |
|
20 |
{ val length: Int = (0 /: body)(_ + _.length) } |
|
63610 | 21 |
case class Atom(length: Int) extends Document |
63605 | 22 |
|
69859 | 23 |
def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean = |
68845
3b2daa7bf9f4
support Thy_Element in Scala, following ML version;
wenzelm
parents:
68840
diff
changeset
|
24 |
command.span.is_kind(keywords, |
3b2daa7bf9f4
support Thy_Element in Scala, following ML version;
wenzelm
parents:
68840
diff
changeset
|
25 |
kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false) |
63605 | 26 |
|
70148 | 27 |
def is_document_command(keywords: Keyword.Keywords, command: Command): Boolean = |
28 |
command.span.is_kind(keywords, Keyword.document, false) |
|
29 |
||
69869 | 30 |
def is_heading_command(command: Command): Boolean = |
31 |
proper_heading_level(command).isDefined |
|
32 |
||
69860 | 33 |
def proper_heading_level(command: Command): Option[Int] = |
69859 | 34 |
command.span.name match { |
35 |
case Thy_Header.CHAPTER => Some(0) |
|
36 |
case Thy_Header.SECTION => Some(1) |
|
37 |
case Thy_Header.SUBSECTION => Some(2) |
|
38 |
case Thy_Header.SUBSUBSECTION => Some(3) |
|
39 |
case Thy_Header.PARAGRAPH => Some(4) |
|
40 |
case Thy_Header.SUBPARAGRAPH => Some(5) |
|
41 |
case _ => None |
|
42 |
} |
|
69860 | 43 |
|
44 |
def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] = |
|
45 |
proper_heading_level(command) orElse |
|
46 |
(if (is_theory_command(keywords, command)) Some(6) else None) |
|
69859 | 47 |
|
63604 | 48 |
|
63606 | 49 |
|
63610 | 50 |
/** context blocks **/ |
63606 | 51 |
|
52 |
def parse_blocks( |
|
53 |
syntax: Outer_Syntax, |
|
54 |
node_name: Document.Node.Name, |
|
55 |
text: CharSequence): List[Document] = |
|
56 |
{ |
|
63607 | 57 |
def is_plain_theory(command: Command): Boolean = |
68840 | 58 |
is_theory_command(syntax.keywords, command) && |
63607 | 59 |
!command.span.is_begin && !command.span.is_end |
60 |
||
61 |
||
63606 | 62 |
/* stack operations */ |
63 |
||
64 |
def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document] |
|
65 |
||
66 |
var stack: List[(Command, mutable.ListBuffer[Document])] = |
|
67 |
List((Command.empty, buffer())) |
|
68 |
||
63607 | 69 |
def open(command: Command) { stack = (command, buffer()) :: stack } |
70 |
||
63606 | 71 |
def close(): Boolean = |
72 |
stack match { |
|
73 |
case (command, body) :: (_, body2) :: _ => |
|
74 |
body2 += Block(command.span.name, command.source, body.toList) |
|
75 |
stack = stack.tail |
|
76 |
true |
|
77 |
case _ => |
|
78 |
false |
|
79 |
} |
|
80 |
||
63607 | 81 |
def flush() { if (is_plain_theory(stack.head._1)) close() } |
82 |
||
63606 | 83 |
def result(): List[Document] = |
84 |
{ |
|
85 |
while (close()) { } |
|
86 |
stack.head._2.toList |
|
87 |
} |
|
88 |
||
89 |
def add(command: Command) |
|
90 |
{ |
|
63607 | 91 |
if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) } |
92 |
else if (command.span.is_end) { flush(); close() } |
|
63606 | 93 |
|
63610 | 94 |
stack.head._2 += Atom(command.source.length) |
63606 | 95 |
} |
96 |
||
97 |
||
98 |
/* result structure */ |
|
99 |
||
100 |
val spans = syntax.parse_spans(text) |
|
101 |
spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span))) |
|
102 |
result() |
|
103 |
} |
|
104 |
||
105 |
||
106 |
||
63610 | 107 |
/** section headings **/ |
108 |
||
109 |
trait Item |
|
63604 | 110 |
{ |
63610 | 111 |
def name: String = "" |
112 |
def source: String = "" |
|
113 |
def heading_level: Option[Int] = None |
|
114 |
} |
|
63604 | 115 |
|
63610 | 116 |
object No_Item extends Item |
63604 | 117 |
|
63610 | 118 |
class Sections(keywords: Keyword.Keywords) |
119 |
{ |
|
120 |
private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document] |
|
63604 | 121 |
|
63610 | 122 |
private var stack: List[(Int, Item, mutable.ListBuffer[Document])] = |
123 |
List((0, No_Item, buffer())) |
|
124 |
||
125 |
@tailrec private def close(level: Int => Boolean) |
|
63604 | 126 |
{ |
127 |
stack match { |
|
63610 | 128 |
case (lev, item, body) :: (_, _, body2) :: _ if level(lev) => |
129 |
body2 += Block(item.name, item.source, body.toList) |
|
63604 | 130 |
stack = stack.tail |
131 |
close(level) |
|
132 |
case _ => |
|
133 |
} |
|
134 |
} |
|
135 |
||
136 |
def result(): List[Document] = |
|
137 |
{ |
|
138 |
close(_ => true) |
|
139 |
stack.head._3.toList |
|
140 |
} |
|
141 |
||
63610 | 142 |
def add(item: Item) |
63604 | 143 |
{ |
63610 | 144 |
item.heading_level match { |
63604 | 145 |
case Some(i) => |
146 |
close(_ > i) |
|
63610 | 147 |
stack = (i + 1, item, buffer()) :: stack |
63604 | 148 |
case None => |
149 |
} |
|
63610 | 150 |
stack.head._3 += Atom(item.source.length) |
63604 | 151 |
} |
63610 | 152 |
} |
63604 | 153 |
|
154 |
||
63610 | 155 |
/* outer syntax sections */ |
156 |
||
157 |
private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item |
|
158 |
{ |
|
159 |
override def name: String = command.span.name |
|
160 |
override def source: String = command.source |
|
69859 | 161 |
override def heading_level: Option[Int] = Document_Structure.heading_level(keywords, command) |
63610 | 162 |
} |
163 |
||
164 |
def parse_sections( |
|
165 |
syntax: Outer_Syntax, |
|
166 |
node_name: Document.Node.Name, |
|
167 |
text: CharSequence): List[Document] = |
|
168 |
{ |
|
169 |
val sections = new Sections(syntax.keywords) |
|
170 |
||
171 |
for { span <- syntax.parse_spans(text) } { |
|
172 |
sections.add( |
|
173 |
new Command_Item(syntax.keywords, |
|
174 |
Command(Document_ID.none, node_name, Command.no_blobs, span))) |
|
175 |
} |
|
176 |
sections.result() |
|
177 |
} |
|
178 |
||
63604 | 179 |
|
63610 | 180 |
/* ML sections */ |
181 |
||
182 |
private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item |
|
183 |
{ |
|
184 |
override def source: String = token.source |
|
185 |
override def heading_level: Option[Int] = level |
|
186 |
} |
|
187 |
||
188 |
def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] = |
|
189 |
{ |
|
190 |
val sections = new Sections(Keyword.Keywords.empty) |
|
191 |
val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None) |
|
192 |
||
193 |
var context: Scan.Line_Context = Scan.Finished |
|
194 |
for (line <- Library.separated_chunks(_ == '\n', text)) { |
|
195 |
val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context) |
|
196 |
val level = |
|
197 |
toks.filterNot(_.is_space) match { |
|
198 |
case List(tok) if tok.is_comment => |
|
199 |
val s = tok.source |
|
64610 | 200 |
if (Codepoint.iterator(s).exists(c => Character.isLetter(c) || Character.isDigit(c))) |
63666 | 201 |
{ |
202 |
if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0) |
|
203 |
else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1) |
|
204 |
else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2) |
|
205 |
else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3) |
|
206 |
else None |
|
207 |
} |
|
63610 | 208 |
else None |
209 |
case _ => None |
|
210 |
} |
|
211 |
if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished) |
|
212 |
toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None))) |
|
213 |
else |
|
214 |
toks.foreach(tok => sections.add(new ML_Item(tok, None))) |
|
215 |
||
216 |
sections.add(nl) |
|
217 |
context = next_context |
|
218 |
} |
|
219 |
sections.result() |
|
63604 | 220 |
} |
221 |
} |