diff --git a/Isa_DOF.thy b/Isa_DOF.thy index d15d08e..4601284 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1,4 +1,4 @@ -chapter \The Document-Type Support Framework for Isabelle \ +chapter \The Document-Type Support Framework for Isabelle\ text{* Offering reflection to ML for class hierarchies, objects and object states. + Isar syntax for these, assuming that classes entities fit to predefined @@ -9,7 +9,7 @@ text{* In this section, we develop on the basis of a management of references Is that provide direct support in the PIDE framework. *} theory Isa_DOF (* Isabelle Document Ontology Framework *) - imports Main (* Isa_MOF *) + imports Main (* Isa_MOF *) keywords "section*" "subsection*" "subsubsection*" "paragraph*" "subparagraph*" "text*" "declare_reference"::thy_decl and diff --git a/converter.scala b/converter.scala index 61e699b..7d7d352 100644 --- a/converter.scala +++ b/converter.scala @@ -21,8 +21,9 @@ case object CURLYCLOSE extends LaTeXToken case object BRACKETOPEN extends LaTeXToken case object BRACKETCLOSE extends LaTeXToken -trait LaTeXCompilationError -case class LaTeXLexerError(msg: String) extends LaTeXCompilationError +sealed trait LaTeXCompilationError +case class LaTeXLexerError (msg: String) extends LaTeXCompilationError +case class LaTeXParserError(msg: String) extends LaTeXCompilationError object LaTeXLexer extends RegexParsers { @@ -183,6 +184,9 @@ def transducer (S:List[LaTeXToken]) : List[LaTeXToken] = /* A more abstract approach, that is based on a two-level parsing approach */ +import scala.util.parsing.combinator.Parsers +import scala.util.parsing.input.{NoPosition, Position, Reader} + object LaTeXParser extends Parsers { override type Elem = LaTeXToken @@ -193,6 +197,20 @@ class LaTeXTokenReader(tokens: Seq[LaTeXToken]) extends Reader[LaTeXToken] { override def rest: Reader[LaTeXToken] = new LaTeXTokenReader(tokens.tail) } +def apply(tokens: Seq[LaTeXToken]): Either[LaTeXParserError, LaTeXToken] = { + val reader = new LaTeXTokenReader(tokens) + program(reader) match { + case NoSuccess(msg, next) => Left(LaTeXParserError(Location(next.pos.line, next.pos.column), msg)) + case Success(result, next) => Right(result) + } + } + + +def program: Parser[LaTeXToken] = positioned { + phrase(block) + } + + } /* Unit Testing Zone */ diff --git a/ontologies/LNCS_onto.thy b/ontologies/LNCS_onto.thy index b89eb90..b739930 100644 --- a/ontologies/LNCS_onto.thy +++ b/ontologies/LNCS_onto.thy @@ -6,15 +6,7 @@ begin doc_class title = short_title :: "string option" -- None - - -(* - -text*[tit::title]{* Using an Ontology Framework*} - -*) - - + doc_class subtitle = abbrev :: "string option" -- None @@ -24,7 +16,7 @@ doc_class author = affiliation :: "string" doc_class abstract = - keywds :: "string list" -- None + keyword_list :: "string list" -- None doc_class text_section = main_author :: "author option" -- None @@ -36,37 +28,13 @@ doc_class technical = text_section + definition_list :: "string list" -- "[]" doc_class example = text_section + - -text*[tit::title]{* Using an Ontology Framework*} - -*) - - -doc_class subtitle = - abbrev :: "string option" -- None - --- \adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \ - -doc_class author = - affiliation :: "string" - -doc_class abstract = - keywds :: "string list" -- None - -doc_class text_section = - main_author :: "author option" -- None - -doc_class introduction = text_section + comment :: string -doc_class technical = text_section + - definition_list :: "string list" -- "[]" - -doc_class example = text_section + - long_name :: "string" -- "'' ''" - doc_class conclusion = text_section + main_author :: "author option" -- None + +doc_class related_work = conclusion + + main_author :: "author option" -- None doc_class bibliography = style :: "string option" -- "''LNCS''" @@ -112,6 +80,7 @@ doc_class article = -- \other idea: capture the essence of a monitor class as trace. trace would be `predefined id` like `main` in C. \ +text{* @{cite bla} *} doc_class article' = trace :: "(title + subtitle + author+ abstract +