Merge branch 'master' of git.logicalhacking.com:HOL-OCL/Isabelle_DOF

document-generator/README.md

@@ -31,7 +31,7 @@ The ``DOF_mkroot`` command takes the same parameter as the standard
 command for building documents can be used. 
 
 Using the ``-o`` option, different LaTeX and ontology setups can be
-selected:
+selected (use ``-h`` to obtain a list of all installed setups):
 ```console 
     -o TEMPLATE  alternative setup for root.tex (default: basic support using scrreprt)
        Available templates:

document-generator/Tools/DOF_mkroot

@@ -38,6 +38,7 @@ function usage()
   echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
   echo
   echo "  Options are:"
+  echo "    -h           print this help text and exit"
   echo "    -d           enable document preparation"
   echo "    -n NAME      alternative session name (default: DIR base name)"
   echo "    -o TEMPLATE  alternative setup for root.tex (default: basic support using scrreprt)"
@@ -68,9 +69,13 @@ DOC=""
 NAME=""
 TEMPLATE="default-scrreprt"
 
-while getopts "o:n:d" OPT
+while getopts "o:n:dh" OPT
 do
   case "$OPT" in
+    h)
+      usage
+      exit 1
+      ;;
     d)
       DOC="true"
       ;;
@@ -82,6 +87,7 @@ do
       ;;
     \?)
       usage
+      exit 0
       ;;
   esac
 done

document-generator/converter/src/main/scala/com/logicalhacking/dof/converter/DofConverter.scala

@@ -104,17 +104,24 @@ object DofConverter {
       }
       
       tail match {
-        case CURLYOPEN::COMMAND("""\isacharcolon""")::CURLYCLOSE :: CURLYOPEN::COMMAND("""\isacharcolon""")::CURLYCLOSE :: tail => {
+        case CURLYOPEN::COMMAND("""\isacharcolon""")::CURLYCLOSE :: CURLYOPEN::COMMAND("""\isacharcolon""")::CURLYCLOSE :: tail  => {
           val (label, shead)= split(List(), head.reverse)
-          val (typ, stail) = split(List(), tail)
+          val (typ, stail) = split(List(), delSpace(tail))
           val typstring = typ match {
             case RAWTEXT(s)::Nil => s.capitalize
             case _          => ""
           }
           (typstring,(shead.reverse)++List(RAWTEXT("""label={"""))++(label.reverse)++List(RAWTEXT("""}, type={"""))++typ++List(RAWTEXT("""}"""))++stail)
         }
+        case CURLYOPEN::COMMAND("""\isacharbrackright""")::CURLYCLOSE :: tail => {
+          val (label, shead)= split(List(), head.reverse)
+          ("",(shead.reverse)++List(RAWTEXT("""label={"""))++(label.reverse)++List(RAWTEXT("""}"""))++List(RAWTEXT("""]"""))++delSpace(tail))
+        }
         case t::tail => convertType(head++List(t), tail)
-        case t => ("",t)
+        case Nil =>  {
+          val (label, shead)= split(List(), head.reverse)
+          ("",(shead.reverse)++List(RAWTEXT("""label={"""))++(label.reverse)++List(RAWTEXT("""}"""))++List(RAWTEXT(""","""))++delSpace(tail))
+        }
       }
     }
 

document-generator/document-template/root-cenelec_50126-scrreprt.tex

@@ -0,0 +1,74 @@
+%% 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}
+\usepackage[utf8]{inputenc}
+\usepackage{textcomp}
+\usepackage[english]{babel}
+\usepackage{isabelle}
+\usepackage{DOF-cenelec_50126}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage[numbers, sort&compress, sectionbib]{natbib}
+\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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%% 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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\title{<TITLE>}
+\author{<AUTHOR>}
+\begin{document}
+\maketitle
+\tableofcontents
+\input{session}
+% optional bibliography
+\IfFileExists{root.bib}{%
+    \bibliographystyle{abbrvnat}
+    \bibliography{root}
+}{}
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:

document-generator/latex/DOF.sty

@@ -52,3 +52,9 @@
     \caption{#1}\label{\commandkey{label}}%
   \end{figure}
 }
+
+\newkeycommand\isaDofText[label=][1]{%
+  \begin{isamarkuptext}%
+      #1
+  \end{isamarkuptext}%
+}

examples/math_exam/BAC2017.thy

@@ -6,7 +6,7 @@ begin
 open_monitor*[exam::MathExam] 
 
 
-section*[idir::Author,affiliation="''CentraleSupelec''", 
+section*[idir::Author,affiliation="''LRI, CentraleSupelec''", 
 email="''idir.aitsadoune@centralesupelec.fr''"]
 {*Idir AIT SADOUNE*}