Upgraded Jenkins build to Isabelle 2018.

.ci/isabelle4isadof/Dockerfile

@@ -24,7 +24,7 @@
 #
 # SPDX-License-Identifier: BSD-2-Clause
 
-FROM logicalhacking:isabelle2017
+FROM logicalhacking:isabelle2018
 
 WORKDIR /home/isabelle
 COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy

Isa_DOF.thy

@@ -1457,10 +1457,8 @@ val _ =
 
 
 end (* struct *)
-
 \<close>
 
-
 ML\<open>
 structure ODL_LTX_Converter = 
 struct
@@ -1474,20 +1472,19 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
                               | SOME(cid,_) => DOF_core.name2doc_class_name thy cid        
         val cid_txt  = "type = " ^ (enclose "{" "}" cid_long);
 
-
-        fun (* ltx_of_term _ _ (((Const ("List.list.Cons", t1) $  (Const ("String.Char", t2 ) $ t))) $ t') 
-                           = (HOLogic.dest_string (((Const ("List.list.Cons", t1) $  (Const ("String.Char", t2 ) $ t))) $ t'))
+        fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2) 
+                  = HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $  t2)
           | ltx_of_term _ _ (Const ("List.list.Nil", _)) = ""
           | ltx_of_term _ _ (@{term "numeral :: _ \<Rightarrow> _"} $ t) = Int.toString(HOLogic.dest_numeral t)
           | ltx_of_term ctx encl ((Const ("List.list.Cons", _) $ t1) $ t2) = 
                                                let val inner = (case t2 of 
-                                                                  Const ("List.list.Nil", _) => (ltx_of_term ctx true t1)
+                                                                  Const ("List.list.Nil", _) =>  (ltx_of_term ctx true t1) 
                                                                 | _ => ((ltx_of_term ctx false t1)^", " ^(ltx_of_term ctx false t2))
                                                              )
                                                in if encl then enclose "{" "}" inner else inner end
           | ltx_of_term _ _ (Const ("Option.option.None", _)) = ""
           | ltx_of_term ctxt _ (Const ("Option.option.Some", _)$t) = ltx_of_term ctxt true t
-          | *)ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
+          | ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
 
 
         fun ltx_of_term_dbg ctx encl term  = let 
@@ -1688,13 +1685,10 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define =
                 val _ = check_and_mark ctxt cid_decl  
                           ({strict_checking = not x}) 
                           (Input.pos_of src) (Input.source_content src) 
-            in  (*(if y then Latex.enclose_block "\\label{" "}" 
-                      else Latex.enclose_block "\\autoref{" "}")
-                [Latex.string (Input.source_content src)]*) 
-                (if y  then Latex.enclose_block ("\\labelX[type="^cid_decl^"]{") "}" 
-                       else Latex.enclose_block ("\\autorefX[type="^cid_decl^"]{") "}")
+            in  
+                (if y  then Latex.enclose_block ("\\csname isadof.label[type={"^cid_decl^"}]{") "}\\endcsname" 
+                       else Latex.enclose_block ("\\csname isadof.ref[type={"^cid_decl^"}]{") "}\\endcsname")
                 [Latex.string (Input.source_content src)] 
-                
             end
           
 

LICENSE

@@ -1,5 +1,6 @@
-Copyright (C) 2018 The University of Sheffield
-              2018 The University of Paris-Sud
+Copyright (C) 2018-2019 The University of Sheffield
+              2019-2019 The University of Exeter
+              2018-2019 The University of Paris-Sud
 All rights reserved.
 
 Redistribution and use in source and binary forms, with or without

document-generator/latex/DOF-COL.sty

@@ -1,5 +1,6 @@
 %% Copyright (C) 2018 The University of Sheffield
 %%               2018 The University of Paris-Sud
+%%               2019 The University of Exeter
 %%
 %% License:
 %%   This program can be redistributed and/or modified under the terms
@@ -50,7 +51,7 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % begin: side_by_side_figure*
-\NewEnviron{isamarkupside_by_side_figure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
+\NewEnviron{isamarkupsideUNDERSCOREbyUNDERSCOREsideUNDERSCOREfigure*}[1][]{\isaDof[env={side_by_side_figure},#1]{\BODY}}
 \newisadof{side_by_side_figure.Isa_COL.side_by_side_figure}%
 [label=,type=%
 ,Isa_COL.figure.relative_width=%

document-generator/latex/DOF-core.sty

@@ -1,5 +1,6 @@
 %% Copyright (C) 2018 The University of Sheffield
 %%               2018 The University of Paris-Sud
+%%               2019 The University of Exeter
 %%
 %% License:
 %%   This program can be redistributed and/or modified under the terms
@@ -126,3 +127,9 @@
 % end: chapter/section default implementations
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% begin: label and ref
+\newisadof{label}[label=,type=][1]{\label{#1}}
+\newisadof{ref}[label=,type=][1]{\autoref{#1}}
+% end: label and ref
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

examples/cenelec/mini_odo/mini_odo.thy

@@ -1,11 +1,7 @@
 
 theory mini_odo
-(*
   imports  "Isabelle_DOF.CENELEC_50128" 
            "Isabelle_DOF.scholarly_paper"
- *)
-  imports  "../../../ontologies/CENELEC_50128" 
-           "../../../ontologies/scholarly_paper"
 
 begin
 
@@ -32,13 +28,13 @@ text\<open>An "anonymous" text-item, automatically coerced into the top-class "t
 text*[tralala] \<open> Brexit means Brexit \<close> 
 
 text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
-     concepts defined in the underlying ontology @{theory "Draft.CENELEC_50128"}. \<close>
+     concepts defined in the underlying ontology @{theory "Isabelle_DOF.CENELEC_50128"}. \<close>
 text*[ass1::assumption] \<open> The subsystem Y is safe. \<close>
 text*[hyp1::hypothesis] \<open> P not equal NP \<close>
   
 text\<open>A real example fragment from a larger project, declaring a text-element as a
      "safety-related application condition", a concept defined in the 
-     @{theory "Draft.CENELEC_50128"} ontology:\<close>  
+     @{theory "Isabelle_DOF.CENELEC_50128"} ontology:\<close>  
 
 text*[new_ass::hypothesis]\<open>Under the assumption @{assumption \<open>ass1\<close>} we establish the following: ... \<close>
 

install

@@ -1,6 +1,7 @@
 #!/usr/bin/env bash
-# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
-#               2018 The University of Paris-Sud. All rights reserved.
+# Copyright (c) 2018-2019 The University of Sheffield.
+#               2019-2019 The University of Exeter. 
+#               2018-2019 The University of Paris-Sud. 
 #
 # Redistribution and use in source and binary forms, with or without
 # modification, are permitted provided that the following conditions

ontologies/scholarly_paper.thy

@@ -65,7 +65,7 @@ doc_class annex = "text_section" +
 
 
 text\<open> Besides subtyping, there is another relation between
-doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
+doc\_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,
 which is expressed by occurrence in the where clause.
 While sub-classing refers to data-inheritance of attributes,
 a monitor captures structural constraints -- the order --