# HG changeset patch # User wenzelm # Date 1470407453 -7200 # Node ID 4b40b8196dc7874e954650b8079f2fc8876c781d # Parent be0a4a0bf7f519fe8841096ddb66e6711c5ae146 Sidekick parser for isabelle-ml and sml mode; diff -r be0a4a0bf7f5 -r 4b40b8196dc7 NEWS --- 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: diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Doc/Implementation/ML.thy --- 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] -\ (*** section ***) +\ (**** chapter ****) + + (*** section ***) (** subsection **) diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Pure/Isar/document_structure.scala --- 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() } } diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Pure/ML/ml_lex.scala --- 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 } diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Tools/jEdit/src/Isabelle.props --- 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 diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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") { diff -r be0a4a0bf7f5 -r 4b40b8196dc7 src/Tools/jEdit/src/services.xml --- 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 @@ new isabelle.jedit.Isabelle_Sidekick_Markup(); + + new isabelle.jedit.Isabelle_Sidekick_ML(); + + + new isabelle.jedit.Isabelle_Sidekick_SML(); + new isabelle.jedit.Isabelle_Sidekick_News();