Conflict resolved.
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
438e8f8e49
|
|
@ -1,7 +1,7 @@
|
|||
theory RegExp
|
||||
imports Main
|
||||
begin
|
||||
|
||||
|
||||
datatype 'a rexp = Empty ("<>")
|
||||
| Atom 'a ("\<lfloor>_\<rfloor>" 65)
|
||||
| Alt "('a rexp)" "('a rexp)" (infixr "||" 55)
|
||||
|
|
@ -110,4 +110,4 @@ by (simp add: epsilonAlt)
|
|||
no_notation Atom ("\<lfloor>_\<rfloor>")
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
299
converter.scala
299
converter.scala
|
|
@ -1,299 +0,0 @@
|
|||
/* Inspired from http://enear.github.io/2016/03/31/parser-combinators/ */
|
||||
|
||||
import scala.util.parsing.combinator._
|
||||
|
||||
sealed trait LaTeXToken
|
||||
|
||||
case class SPACING (str: String) extends LaTeXToken
|
||||
case class RAWTEXT (str: String) extends LaTeXToken
|
||||
case class COMMAND (str: String) extends LaTeXToken
|
||||
case class BEGINENV(prelude: String, str: String) extends LaTeXToken
|
||||
case class ENDENV (prelude: String, str: String) extends LaTeXToken
|
||||
case object VBACKSLASH extends LaTeXToken /* verbatim backslash */
|
||||
case object VSPACE extends LaTeXToken /* verbatim space */
|
||||
case object VTILDE extends LaTeXToken /* verbatim tilde */
|
||||
case object VCURLYOPEN extends LaTeXToken /* verbatim curly bracket open */
|
||||
case object VCURLYCLOSE extends LaTeXToken /* verbatim curly bracket close */
|
||||
case object VBRACKETOPEN extends LaTeXToken /* verbatim square bracket open */
|
||||
case object VBRACKETCLOSE extends LaTeXToken /* verbatim square bracket close */
|
||||
case object CURLYOPEN extends LaTeXToken
|
||||
case object CURLYCLOSE extends LaTeXToken
|
||||
case object BRACKETOPEN extends LaTeXToken
|
||||
case object BRACKETCLOSE extends LaTeXToken
|
||||
|
||||
sealed trait LaTeXCompilationError
|
||||
case class LaTeXLexerError (msg: String) extends LaTeXCompilationError
|
||||
case class LaTeXParserError(msg: String) extends LaTeXCompilationError
|
||||
|
||||
|
||||
object LaTeXLexer extends RegexParsers {
|
||||
|
||||
override def skipWhitespace = false /* No skipping, we want to maintain the layout
|
||||
structure of the LaTeX file */
|
||||
/* override val whiteSpace = "[ \t\r\f]+".r -- probably not usefule here */
|
||||
|
||||
def spacing: Parser[SPACING] = {
|
||||
"[ \t\r\f_]*".r ^^ { str => SPACING(str) }
|
||||
}
|
||||
|
||||
def raw_text: Parser[RAWTEXT] = {
|
||||
"[^\\{\\}\\\\]+".r ^^ { str => RAWTEXT(str) }
|
||||
/* should recognize strings without backslash
|
||||
and without curly bracket { */
|
||||
}
|
||||
|
||||
def begin0: Parser[String] = {
|
||||
"\\\\begin[^\\{]*".r ^^ (_.toString)
|
||||
/* grabs whitespace and also env options ... */
|
||||
}
|
||||
|
||||
def end0: Parser[String] = {
|
||||
"\\\\end[^\\{]*".r ^^ (_.toString)
|
||||
/* grabs whitespace and also env options ... */
|
||||
}
|
||||
|
||||
def arg: Parser[String] = {
|
||||
"\\{[^\\}]*\\}".r ^^ (_.toString)
|
||||
}
|
||||
|
||||
def begin_env = begin0 ~ arg ^^ {case begin_txt ~ arg => BEGINENV(begin_txt,arg)}
|
||||
def end_env = end0 ~ arg ^^ {case end_txt ~ arg => ENDENV (end_txt,arg)}
|
||||
|
||||
def command: Parser[COMMAND] = {
|
||||
"\\\\[a-zA-Z0-9][a-zA-Z0-9*]*".r ^^ { str => COMMAND(str) }
|
||||
}
|
||||
|
||||
def vbackslash = "\\\\" ^^ (_ => VBACKSLASH )
|
||||
def vspace = "\\ " ^^ (_ => VSPACE )
|
||||
def vtilde = "\\~" ^^ (_ => VTILDE )
|
||||
def vcurlyopen = "\\{" ^^ (_ => VCURLYOPEN )
|
||||
def vcurlyclose = "\\}" ^^ (_ => VCURLYCLOSE )
|
||||
def vbracketopen = "\\[" ^^ (_ => VBRACKETOPEN )
|
||||
def vbracketclose = "\\]" ^^ (_ => VBRACKETCLOSE )
|
||||
def curlyopen = "{" ^^ (_ => CURLYOPEN )
|
||||
def curlyclose = "}" ^^ (_ => CURLYCLOSE )
|
||||
def bracketopen = "[" ^^ (_ => BRACKETOPEN )
|
||||
def bracketclose = "]" ^^ (_ => BRACKETCLOSE )
|
||||
|
||||
def tokens: Parser[List[LaTeXToken]] = {
|
||||
phrase(rep1( raw_text |
|
||||
vbackslash | vspace | vtilde |
|
||||
vcurlyopen | vcurlyclose | vbracketopen | vbracketclose |
|
||||
curlyopen | curlyclose | bracketopen | bracketclose |
|
||||
begin_env | end_env | command))
|
||||
}
|
||||
|
||||
def printTokens(tokens: List[LaTeXToken]) : Unit = {
|
||||
tokens.headOption match {
|
||||
|
||||
case Some(SPACING(spaces)) => {println(spaces); printTokens(tokens.tail)}
|
||||
|
||||
case Some(RAWTEXT(txt)) => {println(txt); printTokens(tokens.tail)}
|
||||
|
||||
case Some(COMMAND(txt)) => {println(txt); printTokens(tokens.tail)}
|
||||
|
||||
case Some(BEGINENV(pre,txt)) => {println(pre + txt); printTokens(tokens.tail)}
|
||||
|
||||
case Some(ENDENV(pre,txt)) => {println(pre + txt); printTokens(tokens.tail)}
|
||||
|
||||
case Some(VBACKSLASH) => {println("\\\\"); printTokens(tokens.tail)}
|
||||
case Some(VSPACE) => {println("\\ "); printTokens(tokens.tail)}
|
||||
case Some(VTILDE) => {println("\\~"); printTokens(tokens.tail)}
|
||||
case Some(VCURLYOPEN) => {println("\\{"); printTokens(tokens.tail)}
|
||||
case Some(VCURLYCLOSE) => {println("\\}"); printTokens(tokens.tail)}
|
||||
case Some(VBRACKETOPEN) => {println("\\["); printTokens(tokens.tail)}
|
||||
case Some(VBRACKETCLOSE) => {println("\\]"); printTokens(tokens.tail)}
|
||||
case Some(CURLYOPEN) => {println("{"); printTokens(tokens.tail)}
|
||||
case Some(CURLYCLOSE) => {println("}"); printTokens(tokens.tail)}
|
||||
case Some(BRACKETOPEN) => {println("["); printTokens(tokens.tail)}
|
||||
case Some(BRACKETCLOSE) => {println("]"); printTokens(tokens.tail)}
|
||||
|
||||
case Some(token) => {println("+++ INTERNAL ERROR +++");
|
||||
printTokens(tokens.tail)}
|
||||
|
||||
case None => {println("\n\n")}
|
||||
}
|
||||
}
|
||||
|
||||
def apply(code: String): Either[LaTeXLexerError, List[LaTeXToken]] = {
|
||||
parse(tokens, code) match {
|
||||
case NoSuccess(msg, next) => Left(LaTeXLexerError(msg))
|
||||
case Success(result, next) => Right(result)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/* Some opeations on token streams */
|
||||
|
||||
/* pre: head(S) <> begin */
|
||||
/* post: res = (A,B) where S == A ++ B and
|
||||
where begin@A is a begin-end
|
||||
balanced list if existing,
|
||||
otherwise B = Nil */
|
||||
def parse_group0 (begin:LaTeXToken,end:LaTeXToken, level:Int)
|
||||
(S:List[LaTeXToken])
|
||||
: (List[LaTeXToken],List[LaTeXToken]) = {
|
||||
S match {case Nil => (Nil,Nil)
|
||||
case h1 :: rest if h1 == begin
|
||||
=> (parse_group0 (begin,end, level+1)(rest) match {
|
||||
case (s1, rest2) => (h1 :: s1, rest2)
|
||||
}
|
||||
)
|
||||
case h1 :: rest if h1 == end
|
||||
=> if(level == 0) { (List(h1), rest) }
|
||||
else parse_group0 (begin,end, level-1)(rest) match {
|
||||
case (s1, rest2) => (h1 :: s1, rest2)
|
||||
}
|
||||
case h1 :: rest
|
||||
=> (parse_group0 (begin,end,level)(rest) match {
|
||||
case (s1, rest2) => (h1 :: s1, rest2)
|
||||
}
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
def parse_group (begin:LaTeXToken,end:LaTeXToken)(S:List[LaTeXToken])
|
||||
: (List[LaTeXToken],List[LaTeXToken]) =
|
||||
parse_group0 (begin,end,0)(S) match {
|
||||
case (s1, s2) => (s1.reverse, s2)
|
||||
}
|
||||
|
||||
def purifier (S:List[LaTeXToken]) : List[LaTeXToken] =
|
||||
S match {
|
||||
case RAWTEXT(s1)::CURLYOPEN::COMMAND("\\isacharminus")::CURLYCLOSE ::rest
|
||||
=> purifier(RAWTEXT(s1 + "-") :: rest)
|
||||
case RAWTEXT(s1)::CURLYOPEN::COMMAND("\\isacharunderscore")::CURLYCLOSE::rest
|
||||
=> purifier(RAWTEXT(s1 + "_") :: rest)
|
||||
case COMMAND("\\isacharminus")::CURLYCLOSE::RAWTEXT(s1)::CURLYOPEN::rest
|
||||
=> purifier(RAWTEXT("-" + s1) :: rest)
|
||||
case CURLYOPEN::COMMAND("\\isacharunderscore")::CURLYCLOSE::RAWTEXT(s1)::rest
|
||||
=> purifier(RAWTEXT("_" + s1) :: rest)
|
||||
case RAWTEXT(s1)::RAWTEXT(s2)::rest
|
||||
=> purifier(RAWTEXT(s1 + s2) :: rest)
|
||||
case a :: rest => a :: purifier(rest)
|
||||
case Nil => Nil
|
||||
}
|
||||
|
||||
def transducer (S:List[LaTeXToken]) : List[LaTeXToken] =
|
||||
S match {
|
||||
case COMMAND("\\isacommand")::CURLYOPEN::RAWTEXT(cmd)::CURLYOPEN
|
||||
::COMMAND("\\isacharasterisk")::CURLYCLOSE::CURLYCLOSE
|
||||
::COMMAND("\\isamarkupfalse")::RAWTEXT("%\n"):: CURLYOPEN::rest
|
||||
=> COMMAND("\\"+cmd+"*")::CURLYOPEN::CURLYCLOSE::rest
|
||||
case h :: rest => h :: transducer(rest)
|
||||
case Nil => Nil
|
||||
}
|
||||
|
||||
|
||||
/* 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
|
||||
|
||||
class LaTeXTokenReader(tokens: Seq[LaTeXToken]) extends Reader[LaTeXToken] {
|
||||
override def first: LaTeXToken = tokens.head
|
||||
override def atEnd: Boolean = tokens.isEmpty
|
||||
override def pos: Position = NoPosition
|
||||
override def rest: Reader[LaTeXToken] = new LaTeXTokenReader(tokens.tail)
|
||||
}
|
||||
|
||||
def apply(tokens: Seq[LaTeXToken]): Either[LaTeXParserError, Seq[LaTeXToken]] = {
|
||||
val reader = new LaTeXTokenReader(tokens)
|
||||
parse_latex(reader) match {
|
||||
case NoSuccess(msg, next) => Left(LaTeXParserError(Location(next.pos.line,
|
||||
next.pos.column),
|
||||
msg))
|
||||
case Success(result, next) => Right(result)
|
||||
}
|
||||
}
|
||||
|
||||
def parse_latex(r: Reader[LaTeXToken]) : Parser[Seq[LaTeXToken]] = Success(Nil, Nil)
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
def parse_latex: Parser[Seq[LaTeXToken]] = positioned {
|
||||
phrase(sections)
|
||||
}
|
||||
|
||||
|
||||
def sections: Parser[Seq[LaTeXToken]] = positioned {
|
||||
rep1(section) ^^ { case stmtList => stmtList.flatten }
|
||||
}
|
||||
|
||||
def section: Parser[Seq[LaTeXToken]] = positioned {
|
||||
RAWTEXT() ^^ { case rt @ RAWTEXT (id) => rt::Nil }
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
/* Unit Testing Zone */
|
||||
|
||||
>>> LaTeXLexer("\\\\") => Right(List(VBACKSLASH)) // ok
|
||||
>>> LaTeXLexer("qsdqsd{dfgdfg") => Right(List(RAWTEXT(qsdqsd), CURLYOPEN, RAWTEXT(dfgdfg))) // ok
|
||||
>>> LaTeXLexer("qsdqsd}dfgdfg") => = Right(List(RAWTEXT(qsdqsd), CURLYCLOSE, RAWTEXT(dfgdfg))) // ok
|
||||
>>> LaTeXLexer("qsdqsd\tdfgdfg\n\n \n") => ... // ok
|
||||
>>> LaTeXLexer("qsdqsd\\\\dfgdfg") => Right(List(RAWTEXT(qsdqsd), VBACKSLASH, RAWTEXT(dfgdfg))
|
||||
>>> LaTeXLexer("qsdqsd\\dfgdfg*{sdfsdf}")=> Right(List(RAWTEXT(qsdqsd), COMMAND(\dfgdfg*), CURLYOPEN,
|
||||
RAWTEXT(sdfsdf), CURLYCLOSE)) // ok
|
||||
>>> LaTeXLexer("qsdqsd\\begin [sdgfsdf] {ghjghj}")
|
||||
=> Right(List(RAWTEXT(qsdqsd), BEGINENV(\begin [sdgfsdf] ,{ghjghj})))
|
||||
// ok
|
||||
/* ... but note the following: */
|
||||
>>> LaTeXLexer("qsdqsd\\begin [sdgfsdf] ")
|
||||
=> Right(List(RAWTEXT(qsdqsd), COMMAND(\begin), RAWTEXT( [sdgfsdf] )))
|
||||
|
||||
/* Integration Testing Zone */
|
||||
|
||||
def sample = "\\isacommand{subsubsection{\\isacharasterisk}}\\isamarkupfalse%\n{\\isacharbrackleft}{\\isachardoublequoteopen}Encoder{\\isacharminus}state{\\isacharminus}diagrams{\\isachardoublequoteclose}{\\isacharbrackright}\\ {\\isacharverbatimopen}\\ Encoder\\ State\\ Diagrams\\ {\\isacharverbatimclose}%"
|
||||
|
||||
>>> LaTeXLexer(sample) =>
|
||||
Right(List(COMMAND(\isacommand), CURLYOPEN, RAWTEXT(subsubsection), CURLYOPEN, COMMAND(\isacharasterisk), CURLYCLOSE, CURLYCLOSE, COMMAND(\isamarkupfalse), RAWTEXT(%
|
||||
), CURLYOPEN, COMMAND(\isacharbrackleft), CURLYCLOSE, CURLYOPEN, COMMAND(\isachardoublequoteopen), CURLYCLOSE, RAWTEXT(Encoder), CURLYOPEN, COMMAND(\isacharminus), CURLYCLOSE, RAWTEXT(state), CURLYOPEN, COMMAND(\isacharminus), CURLYCLOSE, RAWTEXT(diagrams), CURLYOPEN, COMMAND(\isachardoublequoteclose), CURLYCLOSE, CURLYOPEN, COMMAND(\isacharbrackright), CURLYCLOSE, VSPACE, CURLYOPEN, COMMAND(\isacharverbatimopen), CURLYCLOSE, VSPACE, RAWTEXT(Encoder), VSPACE, RAWTEXT(State), VSPACE, RAWTEXT(Diagrams), VSPACE, CURLYOPEN, COMMAND(\isacharverbatimclose)...
|
||||
|
||||
|
||||
should become:
|
||||
|
||||
def sample' = "\\isasubsubsection*{Encoder-state-diagrams}{\\ Encoder\\ State\\ Diagrams\\ }"
|
||||
|
||||
which could in the LaTeX be set to:
|
||||
|
||||
def sample'' = "\\isasubsubsection{\\ Encoder\\ State\\ Diagrams\\}\label{sec:Encoder-state-diagrams}"
|
||||
|
||||
def L = List(CURLYOPEN, COMMAND("\\isachardoublequoteopen"), CURLYCLOSE, RAWTEXT("Encoder")
|
||||
, CURLYOPEN, COMMAND("\\isacharminus"), CURLYCLOSE, RAWTEXT("state"), CURLYOPEN, COMMAND("\\isacharminus"), CURLYCLOSE, RAWTEXT("diagrams"), CURLYOPEN, COMMAND("\\isachardoublequoteclose"), CURLYCLOSE, CURLYOPEN, COMMAND("\\isacharbrackright"))
|
||||
|
||||
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
|
||||
|
||||
def sample3 = "\\isacommand{text{\\isacharasterisk}}\\isamarkupfalse%{\\isacharbrackleft}wheel{\\isacharunderscore}ass{\\isacharcolon}{\\isacharcolon}exported{\\isacharunderscore}constraint{\\isacharbrackright}\\ {\\isacharverbatimopen}\\ The\\ number\\ of\\ teeth\\ per\\ wheelturn\\ is\\ assumed\\ to\\ be\\isanewline\\ positive{\\isachardot}{\\isacharverbatimclose}"
|
||||
|
||||
LaTeXLexer(sample3) =>
|
||||
Right(List(COMMAND(\isacommand), CURLYOPEN, RAWTEXT(text), CURLYOPEN, COMMAND(\isacharasterisk), CURLYCLOSE, CURLYCLOSE, COMMAND(\isamarkupfalse), RAWTEXT(%), CURLYOPEN, COMMAND(\isacharbrackleft), CURLYCLOSE, RAWTEXT(wheel), CURLYOPEN, COMMAND(\isacharunderscore), CURLYCLOSE, RAWTEXT(ass), CURLYOPEN, COMMAND(\isacharcolon), CURLYCLOSE, CURLYOPEN, COMMAND(\isacharcolon), CURLYCLOSE, RAWTEXT(exported), CURLYOPEN, COMMAND(\isacharunderscore), CURLYCLOSE, RAWTEXT(constraint), CURLYOPEN, COMMAND(\isacharbrackright), CURLYCLOSE, VSPACE, CURLYOPEN, COMMAND(\isacharverbatimopen), CURLYCLOSE, VSPACE, RAWTEXT(The), VSPACE, RAWTEXT(number), VSPACE, RAWTEXT(of), VSPACE, RAWTEXT(teeth), VSPACE, RAWTEXT(per), VSPACE, RAWTEXT...
|
||||
|
||||
\begin{isamarkuptext*}[wheel_ass::exported_constraint]%
|
||||
\\ The\\ number\\ of\\ teeth\\ per\\ wheelturn\\ is\\ assumed\\ to\\ be\\isanewline\\ positive
|
||||
\end{isamarkuptext*}\isamarkuptrue
|
||||
|
||||
or even:
|
||||
|
||||
\begin{isamarkuptext*}[label=wheel_ass, label_type=exported_constraint, attributes={}]%
|
||||
\\ The\\ number\\ of\\ teeth\\ per\\ wheelturn\\ is\\ assumed\\ to\\ be\\isanewline\\ positive
|
||||
\end{isamarkuptext*}\isamarkuptrue
|
||||
|
||||
|
||||
|
||||
/* Rudimentary Topevel Code */
|
||||
object TestLaTeXLexer extends LaTeXLexer {
|
||||
|
||||
def main(args: Array[String]) = {
|
||||
parse(tokens, "johnny 121") match {
|
||||
case Success(matched,_) => println(matched)
|
||||
case Failure(msg,_) => println("FAILURE: " + msg)
|
||||
case Error(msg,_) => println("ERROR: " + msg)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -1,5 +1,5 @@
|
|||
/**
|
||||
eq * Copyright (c) 2018 The University of Sheffield. All rights reserved.
|
||||
* Copyright (c) 2018 The University of Sheffield. All rights reserved.
|
||||
* 2018 The University of Paris-Sud. All rights reserved.
|
||||
*
|
||||
* Redistribution and use in source and binary forms, with or without
|
||||
|
|
@ -35,56 +35,62 @@ import scala.util.matching.Regex
|
|||
import scala.annotation.tailrec
|
||||
|
||||
object DofConverter {
|
||||
val version = "0.0.0"
|
||||
|
||||
val version = "0.0.2"
|
||||
val sep=RAWTEXT("%\n")
|
||||
|
||||
def deMarkUpArgList(tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
tokens match {
|
||||
case CURLYOPEN :: COMMAND("""\isacharprime""") :: CURLYCLOSE :: CURLYOPEN :: COMMAND("""\isacharprime""") :: CURLYCLOSE :: tail
|
||||
=> RAWTEXT("") :: deMarkUpArgList(tail)
|
||||
case CURLYOPEN :: COMMAND("""\isachardoublequoteopen""") :: CURLYCLOSE :: tail => RAWTEXT("""{""") :: deMarkUpArgList(tail)
|
||||
case CURLYOPEN :: COMMAND("""\isachardoublequoteclose""") :: CURLYCLOSE :: tail => RAWTEXT("""}""") :: deMarkUpArgList(tail)
|
||||
case t :: tail => t :: deMarkUpArgList(tail)
|
||||
case Nil => Nil
|
||||
@tailrec
|
||||
def deMarkUpArgListRec(acc:List[LaTeXToken], tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
val (t,tail) = tokens match {
|
||||
case CURLYOPEN :: COMMAND("""\isacharprime""") :: CURLYCLOSE :: CURLYOPEN :: COMMAND("""\isacharprime""") :: CURLYCLOSE :: tail
|
||||
=> (RAWTEXT(""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isachardoublequoteopen""") :: CURLYCLOSE :: tail => (RAWTEXT("""{"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isachardoublequoteclose""") :: CURLYCLOSE :: tail => (RAWTEXT("""}"""), tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharunderscore""") :: CURLYCLOSE :: tail => (RAWTEXT("""_"""),tail)
|
||||
case t :: tail => (t,tail)
|
||||
case Nil => (RAWTEXT(""),Nil)
|
||||
}
|
||||
if (tokens == Nil) acc
|
||||
else deMarkUpArgListRec(acc++List(t), tail)
|
||||
}
|
||||
deMarkUpArgListRec(Nil, tokens)
|
||||
}
|
||||
|
||||
def deMarkUp(tokens: List[LaTeXToken]): List[LaTeXToken] = deMarkUpT(Nil, tokens)
|
||||
|
||||
@tailrec def deMarkUpT(out:List[LaTeXToken], tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
def matcher(tokens: List[LaTeXToken]): Tuple2[LaTeXToken, List[LaTeXToken]] = {
|
||||
tokens match {
|
||||
case CURLYOPEN :: COMMAND("""\isacharcolon""") :: CURLYCLOSE :: tail => (RAWTEXT(""":"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharunderscore""") :: CURLYCLOSE :: tail => (RAWTEXT("""_"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isadigit""") :: CURLYOPEN::n::CURLYCLOSE::CURLYCLOSE :: tail => (n,tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharcomma""") :: CURLYCLOSE :: tail => (RAWTEXT(""","""),tail)
|
||||
case COMMAND("""\isanewline""") :: tail => (RAWTEXT(""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isachardot""") :: CURLYCLOSE :: tail => (RAWTEXT("""."""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharsemicolon""") :: CURLYCLOSE :: tail => (RAWTEXT(""";"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharbackslash""") :: CURLYCLOSE :: tail => (RAWTEXT("""\"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharslash""") :: CURLYCLOSE :: tail => (RAWTEXT("""/"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharbraceleft""") :: CURLYCLOSE :: tail => (RAWTEXT("""{"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharbraceright""") :: CURLYCLOSE :: tail => (RAWTEXT("""}"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharparenleft""") :: CURLYCLOSE :: tail => (RAWTEXT("""("""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharparenright""") :: CURLYCLOSE :: tail => (RAWTEXT(""")"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharequal""") :: CURLYCLOSE :: tail => (RAWTEXT("""="""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharminus""") :: CURLYCLOSE :: tail => (RAWTEXT("""-"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharplus""") :: CURLYCLOSE :: tail => (RAWTEXT("""+"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharprime""") :: CURLYCLOSE :: tail => (RAWTEXT("""'"""),tail)
|
||||
case VSPACE :: tail => (RAWTEXT(""" """),tail)
|
||||
case t :: tail => (t,tail)
|
||||
case Nil => (RAWTEXT(""" """),Nil)
|
||||
def deMarkUp(tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
@tailrec
|
||||
def deMarkupRec(out:List[LaTeXToken], tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
val (t,tail) = tokens match {
|
||||
case CURLYOPEN :: COMMAND("""\isacharcolon""") :: CURLYCLOSE :: tail => (RAWTEXT(""":"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharunderscore""") :: CURLYCLOSE :: tail => (RAWTEXT("""\_"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isadigit""") :: CURLYOPEN::n::CURLYCLOSE::CURLYCLOSE :: tail => (n,tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharcomma""") :: CURLYCLOSE :: tail => (RAWTEXT(""","""),tail)
|
||||
case COMMAND("""\isanewline""") :: tail => (RAWTEXT(""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isachardot""") :: CURLYCLOSE :: tail => (RAWTEXT("""."""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharsemicolon""") :: CURLYCLOSE :: tail => (RAWTEXT(""";"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharbackslash""") :: CURLYCLOSE :: tail => (RAWTEXT("""\"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharslash""") :: CURLYCLOSE :: tail => (RAWTEXT("""/"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharbraceleft""") :: CURLYCLOSE :: tail => (RAWTEXT("""{"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharbraceright""") :: CURLYCLOSE :: tail => (RAWTEXT("""}"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharparenleft""") :: CURLYCLOSE :: tail => (RAWTEXT("""("""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharparenright""") :: CURLYCLOSE :: tail => (RAWTEXT(""")"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharequal""") :: CURLYCLOSE :: tail => (RAWTEXT("""="""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharminus""") :: CURLYCLOSE :: tail => (RAWTEXT("""-"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharplus""") :: CURLYCLOSE :: tail => (RAWTEXT("""+"""),tail)
|
||||
case CURLYOPEN :: COMMAND("""\isacharprime""") :: CURLYCLOSE :: tail => (RAWTEXT("""'"""),tail)
|
||||
case VSPACE :: tail => (RAWTEXT(""" """),tail)
|
||||
case t :: tail => (t,tail)
|
||||
case Nil => (RAWTEXT(""" """),Nil)
|
||||
}
|
||||
if (tokens == Nil) out
|
||||
else deMarkupRec(out++List(t), tail)
|
||||
}
|
||||
}
|
||||
|
||||
val (t,tail) = matcher(tokens)
|
||||
if (tokens == Nil) out
|
||||
else deMarkUpT(out++List(t), tail)
|
||||
deMarkupRec(Nil, tokens)
|
||||
}
|
||||
|
||||
def convertIsaDofCommand(cmd: String, tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
|
||||
@tailrec
|
||||
def convertType(head: List[LaTeXToken], tail: List[LaTeXToken]): Tuple2[String,List[LaTeXToken]] = {
|
||||
|
||||
@tailrec
|
||||
def split(head:List[LaTeXToken], tokens: List[LaTeXToken]):Tuple2[List[LaTeXToken], List[LaTeXToken]] = {
|
||||
tokens match {
|
||||
case CURLYOPEN::COMMAND("""\isacharcomma""")::CURLYCLOSE::tail => (head,tokens)
|
||||
|
|
@ -96,6 +102,7 @@ object DofConverter {
|
|||
case t => (head,t)
|
||||
}
|
||||
}
|
||||
|
||||
tail match {
|
||||
case CURLYOPEN::COMMAND("""\isacharcolon""")::CURLYCLOSE :: CURLYOPEN::COMMAND("""\isacharcolon""")::CURLYCLOSE :: tail => {
|
||||
val (label, shead)= split(List(), head.reverse)
|
||||
|
|
@ -112,6 +119,7 @@ object DofConverter {
|
|||
}
|
||||
|
||||
|
||||
@tailrec
|
||||
def delSpace(tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
tokens match {
|
||||
case VSPACE :: tail => delSpace(tail)
|
||||
|
|
@ -125,9 +133,8 @@ object DofConverter {
|
|||
}
|
||||
}
|
||||
|
||||
def backSpace(tokens: List[LaTeXToken]): List[LaTeXToken] = (delSpace(tokens.reverse)).reverse
|
||||
|
||||
val sep=RAWTEXT("%\n")
|
||||
def backSpace(tokens: List[LaTeXToken]): List[LaTeXToken] = (delSpace(tokens.reverse)).reverse
|
||||
|
||||
def parseIsaDofCmd(args: List[LaTeXToken], tokens: List[LaTeXToken]): Tuple3[String,List[LaTeXToken], List[LaTeXToken]] = {
|
||||
(args, tokens) match {
|
||||
|
|
@ -150,44 +157,50 @@ object DofConverter {
|
|||
case (args, Nil) => ("",deMarkUp(args), Nil)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
cmd match {
|
||||
val (pre, tail) = cmd match {
|
||||
case """chapter""" => {
|
||||
val (typ,sectionArgs, tail) = parseIsaDofCmd(Nil, tokens)
|
||||
sep::COMMAND("""\isaDofChapter"""+typ) :: sectionArgs ++ convertLaTeXTokenStream(tail)
|
||||
(sep::COMMAND("""\isaDofChapter"""+typ) :: sectionArgs,tail)
|
||||
}
|
||||
case """section""" => {
|
||||
val (typ,sectionArgs, tail) = parseIsaDofCmd(Nil, tokens)
|
||||
sep::COMMAND("""\isaDofSection"""+typ) :: sectionArgs ++ convertLaTeXTokenStream(tail)
|
||||
(sep::COMMAND("""\isaDofSection"""+typ) :: sectionArgs, tail)
|
||||
}
|
||||
case """subsection""" => {
|
||||
val (typ,sectionArgs, tail) = parseIsaDofCmd(Nil, tokens)
|
||||
COMMAND("""\isaDofSubSection"""+typ) :: sectionArgs ++ convertLaTeXTokenStream(tail)
|
||||
(COMMAND("""\isaDofSubSection"""+typ) :: sectionArgs, tail)
|
||||
}
|
||||
case """subsubsection""" => {
|
||||
val (typ,sectionArgs, tail) = parseIsaDofCmd(Nil, tokens)
|
||||
sep::COMMAND("""\isaDofCSubSubSection"""+typ) :: sectionArgs ++ convertLaTeXTokenStream(tail)
|
||||
(sep::COMMAND("""\isaDofSubSubSection"""+typ) :: sectionArgs, tail)
|
||||
}
|
||||
case """paragraph""" => {
|
||||
val (typ,sectionArgs, tail) = parseIsaDofCmd(Nil, tokens)
|
||||
sep::COMMAND("""\isaDofParagraph"""+typ) :: sectionArgs ++ convertLaTeXTokenStream(tail)
|
||||
(sep::COMMAND("""\isaDofParagraph"""+typ) :: sectionArgs, tail)
|
||||
}
|
||||
case """text""" => {
|
||||
val (typ,dofText, tail) = parseIsaDofCmd(Nil, tokens)
|
||||
sep::COMMAND("""\isaDofText"""+typ) :: dofText ++ convertLaTeXTokenStream(tail)
|
||||
(sep::COMMAND("""\isaDofText"""+typ) :: dofText, tail)
|
||||
}
|
||||
case s => sep::COMMAND("""\isaDofUnknown{""" + s + """}""") ::sep:: convertLaTeXTokenStream(tokens)
|
||||
case s => (sep::COMMAND("""\isaDofUnknown{""" + s + """}""")::sep::Nil, tokens)
|
||||
}
|
||||
pre ++ convertLaTeXTokenStream(tail)
|
||||
}
|
||||
|
||||
def convertLaTeXTokenStream(tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
tokens match {
|
||||
case Nil => Nil
|
||||
case COMMAND("""\isacommand""") :: CURLYOPEN :: RAWTEXT(cmd) :: CURLYOPEN
|
||||
:: COMMAND("""\isacharasterisk""") :: CURLYCLOSE :: CURLYCLOSE :: ts => convertIsaDofCommand(cmd, ts)
|
||||
case t :: ts => t :: convertLaTeXTokenStream(ts)
|
||||
@tailrec
|
||||
def convertLaTeXTokenStreamRec(acc: List[LaTeXToken], tokens: List[LaTeXToken]): List[LaTeXToken] = {
|
||||
val (res, tail, rec) = tokens match {
|
||||
case Nil => (Nil, Nil, false)
|
||||
case COMMAND("""\isacommand""") :: CURLYOPEN :: RAWTEXT(cmd) :: CURLYOPEN
|
||||
:: COMMAND("""\isacharasterisk""") :: CURLYCLOSE :: CURLYCLOSE :: ts => (convertIsaDofCommand(cmd, ts), Nil, false)
|
||||
case t :: ts => (t::Nil, ts, true)
|
||||
}
|
||||
if (! rec) acc++res
|
||||
else convertLaTeXTokenStreamRec(acc++res, tail)
|
||||
}
|
||||
convertLaTeXTokenStreamRec(Nil, tokens)
|
||||
}
|
||||
|
||||
def convertLaTeX(string: String): Either[LaTeXLexerError, String] = {
|
||||
|
|
@ -199,8 +212,7 @@ object DofConverter {
|
|||
|
||||
def convertFile(f: File): Option[(String, LaTeXLexerError)] = {
|
||||
val texFileName = f.getAbsolutePath()
|
||||
println("DOF Converter: converting " + texFileName
|
||||
+ " (Not yet fully implemented!)")
|
||||
println("DOF Converter "+version+": converting " + texFileName)
|
||||
f.renameTo(new File(texFileName + ".orig"))
|
||||
|
||||
using(io.Source.fromFile(texFileName + ".orig")) {
|
||||
|
|
@ -259,16 +271,31 @@ object DofConverter {
|
|||
case Some(l) => l
|
||||
}
|
||||
|
||||
val texFiles = directories.map(dir => recursiveListFiles(new File(dir), new Regex("\\.tex$"))
|
||||
.filterNot(_.length() == 0)).flatten
|
||||
val emptyTexFiles = directories.map(dir => recursiveListFiles(new File(dir), new Regex("\\.tex$")).filter(_.length() == 0)).flatten
|
||||
val nonEmptyTexFiles = directories.map(dir => recursiveListFiles(new File(dir), new Regex("\\.tex$")).filterNot(_.length() == 0)).flatten
|
||||
|
||||
if (! emptyTexFiles.isEmpty) {
|
||||
println()
|
||||
println("DOF LaTeX converter warning(s):")
|
||||
println("=============================")
|
||||
println(" Empty LATeX files found, Isabelle build most likely failed!")
|
||||
emptyTexFiles.map { case (file:File) => println(" "+ file + " is empty") }
|
||||
}
|
||||
|
||||
println(texFiles)
|
||||
val errors = texFiles.map(file => convertFile(file)).flatten
|
||||
if (nonEmptyTexFiles.isEmpty) {
|
||||
println()
|
||||
println("DOF LaTeX converter error(s):")
|
||||
println("=============================")
|
||||
println(" No valid LaTeX files found")
|
||||
System.exit(1)
|
||||
}
|
||||
|
||||
val errors = nonEmptyTexFiles.map(file => convertFile(file)).flatten
|
||||
if (!errors.isEmpty) {
|
||||
println()
|
||||
println("DOF LaTeX converter error(s):")
|
||||
println("=============================")
|
||||
errors.map { case (file: String, err: LaTeXLexerError) => println(file + ": " + err) }
|
||||
errors.map { case (file: String, err: LaTeXLexerError) => println(" " + file + ": " + err) }
|
||||
System.exit(1)
|
||||
}
|
||||
System.exit(0)
|
||||
|
|
|
|||
|
|
@ -44,6 +44,11 @@ case class ENDENV (prelude: String, str: String) extends LaTeXToken
|
|||
case object VBACKSLASH extends LaTeXToken /* verbatim backslash */
|
||||
case object VSPACE extends LaTeXToken /* verbatim space */
|
||||
case object VTILDE extends LaTeXToken /* verbatim tilde */
|
||||
case object VHYPHEN extends LaTeXToken
|
||||
case object VCOMMA extends LaTeXToken
|
||||
case object VSEMI extends LaTeXToken
|
||||
case object VQUOTE extends LaTeXToken
|
||||
case object VBACKTICK extends LaTeXToken
|
||||
case object VUNDERSCORE extends LaTeXToken /* verbatim underscore */
|
||||
case object VCURLYOPEN extends LaTeXToken /* verbatim curly bracket open */
|
||||
case object VCURLYCLOSE extends LaTeXToken /* verbatim curly bracket close */
|
||||
|
|
@ -83,7 +88,7 @@ object LaTeXLexer extends RegexParsers {
|
|||
}
|
||||
|
||||
def end0: Parser[String] = {
|
||||
"\\\\end[^\\{]*".r ^^ (_.toString)
|
||||
"\\\\end\\{.*".r ^^ (_.toString)
|
||||
/* grabs whitespace and also env options ... */
|
||||
}
|
||||
|
||||
|
|
@ -101,6 +106,11 @@ object LaTeXLexer extends RegexParsers {
|
|||
def vbackslash = "\\\\" ^^ (_ => VBACKSLASH )
|
||||
def vspace = "\\ " ^^ (_ => VSPACE )
|
||||
def vtilde = "\\~" ^^ (_ => VTILDE )
|
||||
def vhyphen = "\\-" ^^ (_ => VHYPHEN )
|
||||
def vbacktick = "\\`" ^^ (_ => VBACKTICK )
|
||||
def vquote = "\\'" ^^ (_ => VQUOTE )
|
||||
def vsemi = "\\;" ^^ (_ => VSEMI )
|
||||
def vcomma = "\\," ^^ (_ => VCOMMA )
|
||||
def vunderscore = "\\_" ^^ (_ => VUNDERSCORE )
|
||||
def vcurlyopen = "\\{" ^^ (_ => VCURLYOPEN )
|
||||
def vcurlyclose = "\\}" ^^ (_ => VCURLYCLOSE )
|
||||
|
|
@ -114,7 +124,7 @@ object LaTeXLexer extends RegexParsers {
|
|||
|
||||
def tokens: Parser[List[LaTeXToken]] = {
|
||||
phrase(rep1( raw_text |
|
||||
vbackslash | vspace | vtilde | vunderscore |
|
||||
vbackslash | vspace | vtilde | vhyphen | vbacktick | vquote | vsemi | vcomma | vunderscore |
|
||||
vcurlyopen | vcurlyclose | vbracketopen | vbracketclose |
|
||||
curlyopen | curlyclose | bracketopen | bracketclose |
|
||||
newline | begin_env | end_env | command))
|
||||
|
|
@ -143,7 +153,12 @@ object LaTeXLexer extends RegexParsers {
|
|||
case (CURLYCLOSE) => {"""}""" }
|
||||
case (BRACKETOPEN) => {"""[""" }
|
||||
case (BRACKETCLOSE) => {"""]""" }
|
||||
case (token) => {"\n+++ INTERNAL ERROR +++\n"}
|
||||
case (VHYPHEN) => {"""\-"""}
|
||||
case (VBACKTICK) => {"""\`"""}
|
||||
case (VQUOTE) => {"""\'"""}
|
||||
case (VSEMI) => {"""\;"""}
|
||||
case (VCOMMA) => {"""\,"""}
|
||||
case (token) => {"\n+++ INTERNAL ERROR +++\n"}
|
||||
}
|
||||
result += str
|
||||
}
|
||||
|
|
@ -153,7 +168,7 @@ object LaTeXLexer extends RegexParsers {
|
|||
|
||||
def apply(code: String): Either[LaTeXLexerError, List[LaTeXToken]] = {
|
||||
parse(tokens, code) match {
|
||||
case NoSuccess(msg, next) => Left(LaTeXLexerError(msg))
|
||||
case NoSuccess(msg, next) => Left(LaTeXLexerError(msg + " at position "+next.pos))
|
||||
case Success(result, next) => Right(result)
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -69,7 +69,7 @@ fi
|
|||
|
||||
$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar .
|
||||
|
||||
cp $ISABELLE_HOME_USER/DOF/latex/DOF.sty .
|
||||
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
|
||||
|
||||
$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \
|
||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
|
||||
|
|
|
|||
|
|
@ -0,0 +1,14 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
||||
|
||||
%% This is a placeholder for user-specific configuration and packages.
|
||||
|
|
@ -0,0 +1,109 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
||||
|
||||
%% Warning: Do Not Edit!
|
||||
%% =====================
|
||||
%% This is the root file for the Isabelle/DOF configuration "scholarly_paper/lncs".
|
||||
%% All customization and/or additional packages should be added to the file
|
||||
%% preamble.tex.
|
||||
|
||||
\RequirePackage{ifvtex}
|
||||
\documentclass{llncs}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage[USenglish]{babel}
|
||||
\usepackage{isabelle}
|
||||
\usepackage{xcolor}
|
||||
\usepackage{isabellesym}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage[numbers, sort&compress, sectionbib]{natbib}
|
||||
\usepackage{DOF-scholarly_paper-lncs}
|
||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||
\usepackage{xspace}
|
||||
\newcommand{\isadof}{Isabelle/DOF\xspace}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{hyperref}
|
||||
\setcounter{tocdepth}{3}
|
||||
\hypersetup{%
|
||||
bookmarksdepth=3
|
||||
,pdfpagelabels
|
||||
,pageanchor=false
|
||||
,bookmarksnumbered
|
||||
,plainpages=false
|
||||
} % more detailed digital TOC (aka bookmarks)
|
||||
\sloppy
|
||||
\allowdisplaybreaks[4]
|
||||
\urlstyle{rm}
|
||||
\isabellestyle{it}
|
||||
\usepackage[caption]{subfig}
|
||||
\usepackage[size=footnotesize]{caption}
|
||||
|
||||
\newcommand{\ie}{i.e.}
|
||||
\newcommand{\eg}{e.g.}
|
||||
|
||||
\renewcommand{\topfraction}{0.9} % max fraction of floats at top
|
||||
\renewcommand{\bottomfraction}{0.8} % max fraction of floats at bottom
|
||||
\setcounter{topnumber}{2}
|
||||
\setcounter{bottomnumber}{2}
|
||||
\setcounter{totalnumber}{4} % 2 may work better
|
||||
\setcounter{dbltopnumber}{2} % for 2-column pages
|
||||
\renewcommand{\dbltopfraction}{0.9} % fit big float above 2-col. text
|
||||
\renewcommand{\textfraction}{0.07} % allow minimal text w. figs
|
||||
\renewcommand{\floatpagefraction}{0.7} % require fuller float pages
|
||||
\renewcommand{\dblfloatpagefraction}{0.7} % require fuller float pages
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
|
||||
%%% etc. should not be used (they are deprecated since more than a
|
||||
%%% decade)
|
||||
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
|
||||
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
|
||||
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
|
||||
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
|
||||
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\begin{document}
|
||||
\selectlanguage{USenglish}%
|
||||
\renewcommand{\bibname}{References}%
|
||||
\renewcommand{\figurename}{Fig.}
|
||||
\renewcommand{\abstractname}{Abstract.}
|
||||
\renewcommand{\subsubsectionautorefname}{Sect.}
|
||||
\renewcommand{\subsectionautorefname}{Sect.}
|
||||
\renewcommand{\sectionautorefname}{Sect.}
|
||||
\renewcommand{\figureautorefname}{Fig.}
|
||||
\newcommand{\subtableautorefname}{\tableautorefname}
|
||||
\newcommand{\subfigureautorefname}{\figureautorefname}
|
||||
\newcommand{\lstnumberautorefname}{Line}
|
||||
|
||||
|
||||
|
||||
\maketitle
|
||||
\makeatother
|
||||
\input{session}
|
||||
% optional bibliography
|
||||
\IfFileExists{root.bib}{%
|
||||
{\small \renewcommand{\doi}[1]{}
|
||||
\newcommand{\urlprefix}{}
|
||||
|
||||
\bibliographystyle{spmpscinat}
|
||||
|
||||
\bibliography{root}
|
||||
}}{}
|
||||
\end{document}
|
||||
|
||||
%%% Local Variables:
|
||||
%%% mode: latex
|
||||
%%% TeX-master: t
|
||||
%%% End:
|
||||
|
|
@ -1,3 +1,23 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1
|
||||
|
||||
%% Warning: Do Not Edit!
|
||||
%% =====================
|
||||
%% This is the root file for the Isabelle/DOF.
|
||||
%% All customization and/or additional packages should be added to the file
|
||||
%% preamble.tex.
|
||||
|
||||
|
||||
\RequirePackage{ifvtex}
|
||||
\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt}
|
||||
\usepackage[T1]{fontenc}
|
||||
|
|
|
|||
|
|
@ -0,0 +1,45 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{DOF-cenelec_50126}
|
||||
[0000/00/00 Unreleased v0.0.0+%
|
||||
Document-Type Support Framework for Isabelle (CENELEC 50126).]
|
||||
|
||||
\RequirePackage{DOF}
|
||||
|
||||
|
||||
\newkeycommand\isaDofSectionRequirement[label=,type=,main_author=,long_name=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubSectionRequirement[label=,type=,main_author=,long_name=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSectionInterface[label=,type=,main_author=,kind=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
|
||||
\newkeycommand\isaDofTextEc[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextSrac[label=,type=,assumption=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
|
@ -0,0 +1,118 @@
|
|||
%% Copyright (C) 2018 The University of Sheffield
|
||||
%% 2018 The University of Paris-Sud
|
||||
%%
|
||||
%% License:
|
||||
%% This program can be redistributed and/or modified under the terms
|
||||
%% of the LaTeX Project Public License Distributed from CTAN
|
||||
%% archives in directory macros/latex/base/lppl.txt; either
|
||||
%% version 1 of the License, or any later version.
|
||||
%% OR
|
||||
%% The 2-clause BSD-style license.
|
||||
%%
|
||||
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
|
||||
|
||||
\NeedsTeXFormat{LaTeX2e}\relax
|
||||
\ProvidesPackage{DOF-scholarly_paper-lncs}
|
||||
[0000/00/00 Unreleased v0.0.0+%
|
||||
Document-Type Support Framework for Isabelle (LNCS).]
|
||||
|
||||
\RequirePackage{DOF}
|
||||
|
||||
|
||||
\newkeycommand\isaDofSectionIntroduction[label=,type=,main_author=,fixme_list=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSectionExample[label=,type=,main_author=,fixme_list=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSectionTechnical[label=,type=,main_author=,fixme_list=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSectionConclusion[label=,type=,main_author=,fixme_list=][1]{%
|
||||
\isamarkupfalse\isamarkupsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubSectionIntroduction[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubSectionExample[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubSectionTechnical[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofSubSectionConclusion[label=,type=][1]{%
|
||||
\isamarkupfalse\isamarkupsubsection{#1}\label{\commandkey{label}}\isamarkuptrue%
|
||||
}
|
||||
|
||||
|
||||
\newkeycommand\isaDofTextIntroduction[label=,type=,keywordlist=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
#1
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextAbstract[label=,type=,keywordlist=][1]{%
|
||||
\begin{isamarkuptext}%
|
||||
\begin{abstract}%
|
||||
#1%
|
||||
\ifthenelse{\equal{\commandkey{keywordlist}}{}}{}{%
|
||||
\mbox{}\\\medskip\noindent{\textbf{Keywords:}} \commandkey{keywordlist}%
|
||||
}%
|
||||
\end{abstract}%
|
||||
\end{isamarkuptext}%
|
||||
}
|
||||
|
||||
\def\dof@author{}%
|
||||
\def\dof@affiliation{}%
|
||||
|
||||
\AtBeginDocument{%
|
||||
\author{\dof@author}
|
||||
\institute{\dof@affiliation}
|
||||
}
|
||||
|
||||
|
||||
\def\leftadd#1#2{\expandafter\leftaddaux\expandafter{#1}{#2}{#1}}
|
||||
\def\leftaddaux#1#2#3{\gdef#3{#1#2}}
|
||||
|
||||
\newcounter{dof@cnt@author}
|
||||
\newcommand{\addauthor}[1]{%
|
||||
\ifthenelse{\equal{\dof@author}{}}{%
|
||||
\gdef\dof@author{#1}%
|
||||
}{%
|
||||
\leftadd\dof@author{\protect\and #1}%
|
||||
}
|
||||
}
|
||||
|
||||
\newcommand{\addaffiliation}[1]{%
|
||||
\ifthenelse{\equal{\dof@affiliation}{}}{%
|
||||
\gdef\dof@affiliation{#1}%
|
||||
}{%
|
||||
\leftadd\dof@affiliation{\protect\and #1}%
|
||||
}
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextAuthor[label=,type=,email=,affiliation=,orcid=][1]{%
|
||||
\stepcounter{dof@cnt@author}
|
||||
\def\dof@a{\commandkey{affiliation}}
|
||||
\ifthenelse{\equal{\commandkey{orcid}}{}}{%
|
||||
\immediate\write\@auxout{\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}}}%
|
||||
}{%
|
||||
\immediate\write\@auxout{\noexpand\addauthor{#1\noexpand\inst{\thedof@cnt@author}\orcidID{\commandkey{orcid}}}}%
|
||||
}
|
||||
\protected@write\@auxout{}{\string\addaffiliation{\dof@a\\\string\email{\commandkey{email}}}}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextSubtitle[label=,type=,keywordlist=][1]{%
|
||||
\immediate\write\@auxout{\noexpand\subtitle{#1}}%
|
||||
}
|
||||
|
||||
\newkeycommand\isaDofTextTitle[label=,type=,keywordlist=][1]{%
|
||||
\immediate\write\@auxout{\noexpand\title{#1}}%
|
||||
}
|
||||
|
|
@ -16,32 +16,23 @@
|
|||
[0000/00/00 Unreleased v0.0.0+%
|
||||
Document-Type Support Framework for Isabelle.]
|
||||
|
||||
\RequirePackage{keyval}
|
||||
\RequirePackage{environ}
|
||||
\RequirePackage{keycommand}
|
||||
|
||||
\def\dof@label{}%
|
||||
\def\dof@labeltype{}%
|
||||
\def\dof@attributes{}%
|
||||
|
||||
\define@key{dof}{label}{\def\dof@label{#1}}%
|
||||
\define@key{dof}{label_type}{\def\dof@labeltype{#1}}%
|
||||
\define@key{dof}{attributes}{\def\dof@attributes{#1}}%
|
||||
|
||||
|
||||
\NewEnviron{isamarkuptext*}[1][]{%
|
||||
\setkeys{dof}{label=defaultlabel,#1}
|
||||
\centerline{\textsc{Begin Of IsaMarkup Star}}
|
||||
\begin{itemize}
|
||||
\item Arguments:
|
||||
\begin{itemize}
|
||||
\item Label: \dof@label
|
||||
\item label\_type: \dof@labeltype
|
||||
\item attributes: \dof@attributes
|
||||
\end{itemize}
|
||||
\item Body:
|
||||
\BODY
|
||||
\end{itemize}
|
||||
\centerline{\textsc{End Of IsaMarkup Star}}
|
||||
\bigskip
|
||||
\newkeycommand\isaDofChapter[label=,type=][1]{%
|
||||
\isamarkupchapter{#1}\label{\commandkey{label}}%
|
||||
}
|
||||
\newkeycommand\isaDofSection[label=,type=][1]{%
|
||||
\isamarkupsection{#1}\label{\commandkey{label}}%
|
||||
}
|
||||
\newkeycommand\isaDofSubSection[label=,type=][1]{%
|
||||
\isamarkupsubsection{#1}\label{\commandkey{label}}%
|
||||
}
|
||||
\newkeycommand\isaDofSubSubSection[label=,type=][1]{%
|
||||
\isamarkupsubsubsection{#1}\label{\commandkey{label}}%
|
||||
}
|
||||
\newkeycommand\isaDofParagraph[label=,type=][1]{%
|
||||
\isamarkupparagraph{#1}\label{\commandkey{label}}%
|
||||
}
|
||||
\newkeycommand\isaDofSubParagraph[label=,type=][1]{%
|
||||
\isamarkupsubparagraph{#1}\label{\commandkey{label}}%
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,19 +0,0 @@
|
|||
\documentclass{article}
|
||||
\usepackage{DOF}
|
||||
\begin{document}
|
||||
|
||||
\begin{isamarkuptext*}[label=wheel\_ass, label_type=exported\_constraint, attributes={}]%
|
||||
The\ number\ of\ teeth\ per\ wheelturn\ is\ assumed\ to\ be\ positive.
|
||||
\end{isamarkuptext*}
|
||||
|
||||
\begin{isamarkuptext*}[label=wheel\_ass, attributes={}]%
|
||||
The\ number\ of\ teeth\ per\ wheelturn\ is\ assumed\ to\ be\ positive.
|
||||
\end{isamarkuptext*}
|
||||
|
||||
\begin{isamarkuptext*}[attributes={foo\_attribute}]%
|
||||
The\ number\ of\ teeth\ per\ wheelturn\ is\ assumed\ to\ be\ positive.
|
||||
\end{isamarkuptext*}
|
||||
|
||||
\end{document}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue