Kleinkram

- ein paar Elemente im Parser
- neue tests im Exampl

CENELEC_50126.thy

@@ -159,7 +159,7 @@ to a test-environment or test-engine *}
 text \<open> As established by @{docref \<open>t10\<close>}, the 
        assumption @{docref \<open>ass122\<close>} is validated. \<close>
 
-
+                               
 section{* Provisory Setup *}
 
 (* Hack: This should be generated automatically: *)

converter.scala

@@ -181,6 +181,20 @@ def transducer (S:List[LaTeXToken]) : List[LaTeXToken] =
       case Nil => Nil
     }
 
+/* A more abstract approach, that is based on a two-level parsing approach */
+
+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)
+}
+
+}
+
 /* Unit Testing Zone */
 
 >>>  LaTeXLexer("\\\\")                   => Right(List(VBACKSLASH)) // ok

examples/simple/Example.thy

@@ -24,9 +24,10 @@ declare_reference [lalala::requirement, alpha="main", beta=42]
 
 declare_reference [lalala::quod] (* shouldn't work *)
 
-declare_reference [blablabla::cid, alpha=beta, beta=gamma]
+declare_reference [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
   
 paragraph*[sdf]{* just a paragraph *}  
+paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>  
 
 subsection*[sdf]{* shouldn't work, multiple ref. *}