Sidekick parser for isabelle-ml and sml mode;
authorwenzelm
Fri Aug 05 16:30:53 2016 +0200 (2016-08-05)
changeset 636104b40b8196dc7
parent 63609 be0a4a0bf7f5
child 63611 fb63942e470e
Sidekick parser for isabelle-ml and sml mode;
NEWS
src/Doc/Implementation/ML.thy
src/Pure/Isar/document_structure.scala
src/Pure/ML/ml_lex.scala
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/NEWS	Thu Aug 04 21:30:20 2016 +0200
     1.2 +++ b/NEWS	Fri Aug 05 16:30:53 2016 +0200
     1.3 @@ -63,6 +63,10 @@
     1.4  * Cartouche abbreviations work both for " and ` to accomodate typical
     1.5  situations where old ASCII notation may be updated.
     1.6  
     1.7 +* Isabelle/ML and Standard ML files are presented in Sidekick with the
     1.8 +tree structure of section headings: this special comment format is
     1.9 +described in "implementation" chapter 0, e.g. (*** section ***).
    1.10 +
    1.11  * IDE support for the Isabelle/Pure bootstrap process, with the
    1.12  following independent stages:
    1.13  
     2.1 --- a/src/Doc/Implementation/ML.thy	Thu Aug 04 21:30:20 2016 +0200
     2.2 +++ b/src/Doc/Implementation/ML.thy	Fri Aug 05 16:30:53 2016 +0200
     2.3 @@ -70,11 +70,14 @@
     2.4    prose description of the purpose of the module. The latter can range from a
     2.5    single line to several paragraphs of explanations.
     2.6  
     2.7 -  The rest of the file is divided into sections, subsections, subsubsections,
     2.8 -  paragraphs etc.\ using a simple layout via ML comments as follows.
     2.9 +  The rest of the file is divided into chapters, sections, subsections,
    2.10 +  subsubsections, paragraphs etc.\ using a simple layout via ML comments as
    2.11 +  follows.
    2.12  
    2.13    @{verbatim [display]
    2.14 -\<open>  (*** section ***)
    2.15 +\<open>  (**** chapter ****)
    2.16 + 
    2.17 +  (*** section ***)
    2.18  
    2.19    (** subsection **)
    2.20  
     3.1 --- a/src/Pure/Isar/document_structure.scala	Thu Aug 04 21:30:20 2016 +0200
     3.2 +++ b/src/Pure/Isar/document_structure.scala	Fri Aug 05 16:30:53 2016 +0200
     3.3 @@ -13,14 +13,12 @@
     3.4  
     3.5  object Document_Structure
     3.6  {
     3.7 -  /* general structure */
     3.8 +  /** general structure **/
     3.9  
    3.10    sealed abstract class Document { def length: Int }
    3.11    case class Block(name: String, text: String, body: List[Document]) extends Document
    3.12    { val length: Int = (0 /: body)(_ + _.length) }
    3.13 -  case class Atom(command: Command) extends Document
    3.14 -  { def length: Int = command.length }
    3.15 -
    3.16 +  case class Atom(length: Int) extends Document
    3.17  
    3.18    private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean =
    3.19      keywords.kinds.get(name) match {
    3.20 @@ -28,23 +26,9 @@
    3.21        case None => false
    3.22      }
    3.23  
    3.24 -  private def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    3.25 -  {
    3.26 -    val name = command.span.name
    3.27 -    name match {
    3.28 -      case Thy_Header.CHAPTER => Some(0)
    3.29 -      case Thy_Header.SECTION => Some(1)
    3.30 -      case Thy_Header.SUBSECTION => Some(2)
    3.31 -      case Thy_Header.SUBSUBSECTION => Some(3)
    3.32 -      case Thy_Header.PARAGRAPH => Some(4)
    3.33 -      case Thy_Header.SUBPARAGRAPH => Some(5)
    3.34 -      case _ if is_theory_command(keywords, name) => Some(6)
    3.35 -      case _ => None
    3.36 -    }
    3.37 -  }
    3.38  
    3.39  
    3.40 -  /* context blocks */
    3.41 +  /** context blocks **/
    3.42  
    3.43    def parse_blocks(
    3.44      syntax: Outer_Syntax,
    3.45 @@ -88,7 +72,7 @@
    3.46        if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
    3.47        else if (command.span.is_end) { flush(); close() }
    3.48  
    3.49 -      stack.head._2 += Atom(command)
    3.50 +      stack.head._2 += Atom(command.source.length)
    3.51      }
    3.52  
    3.53  
    3.54 @@ -100,25 +84,30 @@
    3.55    }
    3.56  
    3.57  
    3.58 -  /* section headings etc. */
    3.59  
    3.60 -  def parse_sections(
    3.61 -    syntax: Outer_Syntax,
    3.62 -    node_name: Document.Node.Name,
    3.63 -    text: CharSequence): List[Document] =
    3.64 +  /** section headings **/
    3.65 +
    3.66 +  trait Item
    3.67    {
    3.68 -    /* stack operations */
    3.69 +    def name: String = ""
    3.70 +    def source: String = ""
    3.71 +    def heading_level: Option[Int] = None
    3.72 +  }
    3.73  
    3.74 -    def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    3.75 +  object No_Item extends Item
    3.76  
    3.77 -    var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
    3.78 -      List((0, Command.empty, buffer()))
    3.79 +  class Sections(keywords: Keyword.Keywords)
    3.80 +  {
    3.81 +    private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    3.82  
    3.83 -    @tailrec def close(level: Int => Boolean)
    3.84 +    private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
    3.85 +      List((0, No_Item, buffer()))
    3.86 +
    3.87 +    @tailrec private def close(level: Int => Boolean)
    3.88      {
    3.89        stack match {
    3.90 -        case (lev, command, body) :: (_, _, body2) :: _ if level(lev) =>
    3.91 -          body2 += Block(command.span.name, command.source, body.toList)
    3.92 +        case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
    3.93 +          body2 += Block(item.name, item.source, body.toList)
    3.94            stack = stack.tail
    3.95            close(level)
    3.96          case _ =>
    3.97 @@ -131,22 +120,91 @@
    3.98        stack.head._3.toList
    3.99      }
   3.100  
   3.101 -    def add(command: Command)
   3.102 +    def add(item: Item)
   3.103      {
   3.104 -      heading_level(syntax.keywords, command) match {
   3.105 +      item.heading_level match {
   3.106          case Some(i) =>
   3.107            close(_ > i)
   3.108 -          stack = (i + 1, command, buffer()) :: stack
   3.109 +          stack = (i + 1, item, buffer()) :: stack
   3.110          case None =>
   3.111        }
   3.112 -      stack.head._3 += Atom(command)
   3.113 +      stack.head._3 += Atom(item.source.length)
   3.114      }
   3.115 +  }
   3.116  
   3.117  
   3.118 -    /* result structure */
   3.119 +  /* outer syntax sections */
   3.120 +
   3.121 +  private class Command_Item(keywords: Keyword.Keywords, command: Command) extends Item
   3.122 +  {
   3.123 +    override def name: String = command.span.name
   3.124 +    override def source: String = command.source
   3.125 +    override def heading_level: Option[Int] =
   3.126 +    {
   3.127 +      name match {
   3.128 +        case Thy_Header.CHAPTER => Some(0)
   3.129 +        case Thy_Header.SECTION => Some(1)
   3.130 +        case Thy_Header.SUBSECTION => Some(2)
   3.131 +        case Thy_Header.SUBSUBSECTION => Some(3)
   3.132 +        case Thy_Header.PARAGRAPH => Some(4)
   3.133 +        case Thy_Header.SUBPARAGRAPH => Some(5)
   3.134 +        case _ if is_theory_command(keywords, name) => Some(6)
   3.135 +        case _ => None
   3.136 +      }
   3.137 +    }
   3.138 +  }
   3.139 +
   3.140 +  def parse_sections(
   3.141 +    syntax: Outer_Syntax,
   3.142 +    node_name: Document.Node.Name,
   3.143 +    text: CharSequence): List[Document] =
   3.144 +  {
   3.145 +    val sections = new Sections(syntax.keywords)
   3.146 +
   3.147 +    for { span <- syntax.parse_spans(text) } {
   3.148 +      sections.add(
   3.149 +        new Command_Item(syntax.keywords,
   3.150 +          Command(Document_ID.none, node_name, Command.no_blobs, span)))
   3.151 +    }
   3.152 +    sections.result()
   3.153 +  }
   3.154 +
   3.155  
   3.156 -    val spans = syntax.parse_spans(text)
   3.157 -    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
   3.158 -    result()
   3.159 +  /* ML sections */
   3.160 +
   3.161 +  private class ML_Item(token: ML_Lex.Token, level: Option[Int]) extends Item
   3.162 +  {
   3.163 +    override def source: String = token.source
   3.164 +    override def heading_level: Option[Int] = level
   3.165 +  }
   3.166 +
   3.167 +  def parse_ml_sections(SML: Boolean, text: CharSequence): List[Document] =
   3.168 +  {
   3.169 +    val sections = new Sections(Keyword.Keywords.empty)
   3.170 +    val nl = new ML_Item(ML_Lex.Token(ML_Lex.Kind.SPACE, "\n"), None)
   3.171 +
   3.172 +    var context: Scan.Line_Context = Scan.Finished
   3.173 +    for (line <- Library.separated_chunks(_ == '\n', text)) {
   3.174 +      val (toks, next_context) = ML_Lex.tokenize_line(SML, line, context)
   3.175 +      val level =
   3.176 +        toks.filterNot(_.is_space) match {
   3.177 +          case List(tok) if tok.is_comment =>
   3.178 +            val s = tok.source
   3.179 +            if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
   3.180 +            else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
   3.181 +            else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
   3.182 +            else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
   3.183 +            else None
   3.184 +          case _ => None
   3.185 +        }
   3.186 +      if (level.isDefined && context == Scan.Finished && next_context == Scan.Finished)
   3.187 +        toks.foreach(tok => sections.add(new ML_Item(tok, if (tok.is_comment) level else None)))
   3.188 +      else
   3.189 +        toks.foreach(tok => sections.add(new ML_Item(tok, None)))
   3.190 +
   3.191 +      sections.add(nl)
   3.192 +      context = next_context
   3.193 +    }
   3.194 +    sections.result()
   3.195    }
   3.196  }
     4.1 --- a/src/Pure/ML/ml_lex.scala	Thu Aug 04 21:30:20 2016 +0200
     4.2 +++ b/src/Pure/ML/ml_lex.scala	Fri Aug 05 16:30:53 2016 +0200
     4.3 @@ -66,6 +66,8 @@
     4.4    {
     4.5      def is_keyword: Boolean = kind == Kind.KEYWORD
     4.6      def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
     4.7 +    def is_space: Boolean = kind == Kind.SPACE
     4.8 +    def is_comment: Boolean = kind == Kind.COMMENT
     4.9    }
    4.10  
    4.11  
     5.1 --- a/src/Tools/jEdit/src/Isabelle.props	Thu Aug 04 21:30:20 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Fri Aug 05 16:30:53 2016 +0200
     5.3 @@ -87,7 +87,8 @@
     5.4  mode.isabelle.folding=isabelle
     5.5  mode.isabelle.sidekick.parser=isabelle
     5.6  mode.isabelle.sidekick.showStatusWindow.label=true
     5.7 -mode.ml.sidekick.parser=isabelle
     5.8 +mode.isabelle-ml.sidekick.parser=isabelle-ml
     5.9 +mode.sml.sidekick.parser=isabelle-sml
    5.10  sidekick.parser.isabelle.label=Isabelle
    5.11  mode.bibtex.folding=sidekick
    5.12  mode.bibtex.sidekick.parser=bibtex
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 21:30:20 2016 +0200
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Aug 05 16:30:53 2016 +0200
     6.3 @@ -146,26 +146,32 @@
     6.4    }
     6.5  }
     6.6  
     6.7 -
     6.8  class Isabelle_Sidekick_Default extends
     6.9    Isabelle_Sidekick_Structure("isabelle",
    6.10      PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
    6.11  
    6.12 -
    6.13  class Isabelle_Sidekick_Context extends
    6.14    Isabelle_Sidekick_Structure("isabelle-context",
    6.15      PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
    6.16  
    6.17 -
    6.18  class Isabelle_Sidekick_Options extends
    6.19    Isabelle_Sidekick_Structure("isabelle-options",
    6.20      _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
    6.21  
    6.22 -
    6.23  class Isabelle_Sidekick_Root extends
    6.24    Isabelle_Sidekick_Structure("isabelle-root",
    6.25      _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
    6.26  
    6.27 +class Isabelle_Sidekick_ML extends
    6.28 +  Isabelle_Sidekick_Structure("isabelle-ml",
    6.29 +    buffer => Some(PIDE.resources.node_name(buffer)),
    6.30 +    (_, _, text) => Document_Structure.parse_ml_sections(false, text))
    6.31 +
    6.32 +class Isabelle_Sidekick_SML extends
    6.33 +  Isabelle_Sidekick_Structure("isabelle-sml",
    6.34 +    buffer => Some(PIDE.resources.node_name(buffer)),
    6.35 +    (_, _, text) => Document_Structure.parse_ml_sections(true, text))
    6.36 +
    6.37  
    6.38  class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
    6.39  {
     7.1 --- a/src/Tools/jEdit/src/services.xml	Thu Aug 04 21:30:20 2016 +0200
     7.2 +++ b/src/Tools/jEdit/src/services.xml	Fri Aug 05 16:30:53 2016 +0200
     7.3 @@ -23,6 +23,12 @@
     7.4    <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
     7.5      new isabelle.jedit.Isabelle_Sidekick_Markup();
     7.6    </SERVICE>
     7.7 +  <SERVICE NAME="isabelle-ml" CLASS="sidekick.SideKickParser">
     7.8 +    new isabelle.jedit.Isabelle_Sidekick_ML();
     7.9 +  </SERVICE>
    7.10 +  <SERVICE NAME="isabelle-sml" CLASS="sidekick.SideKickParser">
    7.11 +    new isabelle.jedit.Isabelle_Sidekick_SML();
    7.12 +  </SERVICE>
    7.13    <SERVICE NAME="isabelle-news" CLASS="sidekick.SideKickParser">
    7.14      new isabelle.jedit.Isabelle_Sidekick_News();
    7.15    </SERVICE>