--- a/NEWS Thu Aug 04 21:30:20 2016 +0200
+++ b/NEWS Fri Aug 05 16:30:53 2016 +0200
@@ -63,6 +63,10 @@
* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.
+* Isabelle/ML and Standard ML files are presented in Sidekick with the
+tree structure of section headings: this special comment format is
+described in "implementation" chapter 0, e.g. (*** section ***).
+
* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:
--- a/src/Doc/Implementation/ML.thy Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Fri Aug 05 16:30:53 2016 +0200
@@ -70,11 +70,14 @@
prose description of the purpose of the module. The latter can range from a
single line to several paragraphs of explanations.
- The rest of the file is divided into sections, subsections, subsubsections,
- paragraphs etc.\ using a simple layout via ML comments as follows.
+ The rest of the file is divided into chapters, sections, subsections,
+ subsubsections, paragraphs etc.\ using a simple layout via ML comments as
+ follows.
@{verbatim [display]
-\<open> (*** section ***)
+\<open> (**** chapter ****)
+
+ (*** section ***)
(** subsection **)
--- a/src/Pure/Isar/document_structure.scala Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Pure/Isar/document_structure.scala Fri Aug 05 16:30:53 2016 +0200
@@ -13,14 +13,12 @@
object Document_Structure
{
- /* general structure */
+ /** general structure **/
sealed abstract class Document { def length: Int }
case class Block(name: String, text: String, body: List[Document]) extends Document
{ val length: Int = (0 /: body)(_ + _.length) }
- case class Atom(command: Command) extends Document
- { def length: Int = command.length }
-
+ case class Atom(length: Int) extends Document
private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean =
keywords.kinds.get(name) match {
@@ -28,23 +26,9 @@
case None => false
}
- private def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
- {
- val name = command.span.name
- name match {
- case Thy_Header.CHAPTER => Some(0)
- case Thy_Header.SECTION => Some(1)
- case Thy_Header.SUBSECTION => Some(2)
- case Thy_Header.SUBSUBSECTION => Some(3)
- case Thy_Header.PARAGRAPH => Some(4)
- case Thy_Header.SUBPARAGRAPH => Some(5)
- case _ if is_theory_command(keywords, name) => Some(6)
- case _ => None
- }
- }
- /* context blocks */
+ /** context blocks **/
def parse_blocks(
syntax: Outer_Syntax,
@@ -88,7 +72,7 @@
if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
else if (command.span.is_end) { flush(); close() }
- stack.head._2 += Atom(command)
+ stack.head._2 += Atom(command.source.length)
}
@@ -100,25 +84,30 @@
}
- /* section headings etc. */
- def parse_sections(
- syntax: Outer_Syntax,
- node_name: Document.Node.Name,
- text: CharSequence): List[Document] =
+ /** section headings **/
+
+ trait Item
{
- /* stack operations */
+ def name: String = ""
+ def source: String = ""
+ def heading_level: Option[Int] = None
+ }
- def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
+ object No_Item extends Item
- var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
- List((0, Command.empty, buffer()))
+ class Sections(keywords: Keyword.Keywords)
+ {
+ private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
- @tailrec def close(level: Int => Boolean)
+ private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
+ List((0, No_Item, buffer()))
+
+ @tailrec private def close(level: Int => Boolean)
{
stack match {
- case (lev, command, body) :: (_, _, body2) :: _ if level(lev) =>
- body2 += Block(command.span.name, command.source, body.toList)
+ case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
+ body2 += Block(item.name, item.source, body.toList)
stack = stack.tail
close(level)
case _ =>
@@ -131,22 +120,91 @@
stack.head._3.toList
}
- def add(command: Command)
+ def add(item: Item)
{
- heading_level(syntax.keywords, command) match {
+ item.heading_level match {
case Some(i) =>
close(_ > i)
- stack = (i + 1, command, buffer()) :: stack
+ stack = (i + 1, item, buffer()) :: stack
case None =>
}
- stack.head._3 += Atom(command)
+ stack.head._3 += Atom(item.source.length)
}
+ }
- /* result structure */
+ /* outer syntax sections */
+
+ private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item
+ {
+ override def name: String = command.span.name
+ override def source: String = command.source
+ override def heading_level: Option[Int] =
+ {
+ name match {
+ case Thy_Header.CHAPTER => Some(0)
+ case Thy_Header.SECTION => Some(1)
+ case Thy_Header.SUBSECTION => Some(2)
+ case Thy_Header.SUBSUBSECTION => Some(3)
+ case Thy_Header.PARAGRAPH => Some(4)
+ case Thy_Header.SUBPARAGRAPH => Some(5)
+ case _ if is_theory_command(keywords, name) => Some(6)
+ case _ => None
+ }
+ }
+ }
+
+ def parse_sections(
+ syntax: Outer_Syntax,
+ node_name: Document.Node.Name,
+ text: CharSequence): List[Document] =
+ {
+ val sections = new Sections(syntax.keywords)
+
+ for { span <- syntax.parse_spans(text) } {
+ sections.add(
+ new Command_Item(syntax.keywords,
+ Command(Document_ID.none, node_name, Command.no_blobs, span)))
+ }
+ sections.result()
+ }
+
- val spans = syntax.parse_spans(text)
- spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
- result()
+ /* ML sections */
+
+ private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item
+ {
+ override def source: String = token.source
+ override def heading_level: Option[Int] = level
+ }
+
+ def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] =
+ {
+ val sections = new Sections(Keyword.Keywords.empty)
+ val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)
+
+ var context: Scan.Line_Context = Scan.Finished
+ for (line <- Library.separated_chunks(_ == '\n', text)) {
+ val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context)
+ val level =
+ toks.filterNot(_.is_space) match {
+ case List(tok) if tok.is_comment =>
+ val s = tok.source
+ if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
+ else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
+ else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
+ else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
+ else None
+ case _ => None
+ }
+ if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished)
+ toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None)))
+ else
+ toks.foreach(tok => sections.add(new ML_Item(tok, None)))
+
+ sections.add(nl)
+ context = next_context
+ }
+ sections.result()
}
}
--- a/src/Pure/ML/ml_lex.scala Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Pure/ML/ml_lex.scala Fri Aug 05 16:30:53 2016 +0200
@@ -66,6 +66,8 @@
{
def is_keyword: Boolean = kind == Kind.KEYWORD
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
+ def is_space: Boolean = kind == Kind.SPACE
+ def is_comment: Boolean = kind == Kind.COMMENT
}
--- a/src/Tools/jEdit/src/Isabelle.props Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Fri Aug 05 16:30:53 2016 +0200
@@ -87,7 +87,8 @@
mode.isabelle.folding=isabelle
mode.isabelle.sidekick.parser=isabelle
mode.isabelle.sidekick.showStatusWindow.label=true
-mode.ml.sidekick.parser=isabelle
+mode.isabelle-ml.sidekick.parser=isabelle-ml
+mode.sml.sidekick.parser=isabelle-sml
sidekick.parser.isabelle.label=Isabelle
mode.bibtex.folding=sidekick
mode.bibtex.sidekick.parser=bibtex
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Aug 05 16:30:53 2016 +0200
@@ -146,26 +146,32 @@
}
}
-
class Isabelle_Sidekick_Default extends
Isabelle_Sidekick_Structure("isabelle",
PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
-
class Isabelle_Sidekick_Context extends
Isabelle_Sidekick_Structure("isabelle-context",
PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
-
class Isabelle_Sidekick_Options extends
Isabelle_Sidekick_Structure("isabelle-options",
_ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
-
class Isabelle_Sidekick_Root extends
Isabelle_Sidekick_Structure("isabelle-root",
_ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
+class Isabelle_Sidekick_ML extends
+ Isabelle_Sidekick_Structure("isabelle-ml",
+ buffer => Some(PIDE.resources.node_name(buffer)),
+ (_, _, text) => Document_Structure.parse_ml_sections(false, text))
+
+class Isabelle_Sidekick_SML extends
+ Isabelle_Sidekick_Structure("isabelle-sml",
+ buffer => Some(PIDE.resources.node_name(buffer)),
+ (_, _, text) => Document_Structure.parse_ml_sections(true, text))
+
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
{
--- a/src/Tools/jEdit/src/services.xml Thu Aug 04 21:30:20 2016 +0200
+++ b/src/Tools/jEdit/src/services.xml Fri Aug 05 16:30:53 2016 +0200
@@ -23,6 +23,12 @@
<SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Markup();
</SERVICE>
+ <SERVICE NAME="isabelle-ml" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_ML();
+ </SERVICE>
+ <SERVICE NAME="isabelle-sml" CLASS="sidekick.SideKickParser">
+ new isabelle.jedit.Isabelle_Sidekick_SML();
+ </SERVICE>
<SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_News();
</SERVICE>