always allow plugins

META.in

@@ -2,4 +2,4 @@ description = "The Why3 Ocaml library"
 version = "@VERSION@"
 archive(byte) = "why3.cma"
 archive(native) = "why3.cmxa"
-requires = "str unix num @META_DYNLINK@ @META_OCAMLGRAPH@"
+requires = "str unix num dynlink @META_OCAMLGRAPH@"

Makefile.in

@@ -82,7 +82,7 @@ endif
 # external libraries common to all binaries
 
 EXTOBJS =
-EXTLIBS = str unix nums @META_DYNLINK@
+EXTLIBS = str unix nums dynlink
 
 EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
 EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
@@ -994,8 +994,6 @@ bts12244: src/why3.cma
 
 ## Examples : Plugins ##
 
-ifeq (@enable_plugins@,yes)
-
 PLUGDIR = examples/plugins/
 PLUG_FILES = genequlin
 
@@ -1035,8 +1033,6 @@ clean::
 	rm -f $(PLUGGENERATED)
 	rm -f .depend.plug
 
-endif
-
 ################
 # documentation
 ################

configure.in

@@ -17,10 +17,9 @@
 #                                                                        #
 ##########################################################################
 
-
 #
 # autoconf input for Objective Caml programs
-# Copyright (C) 2001 Jean-Christophe Fillitre
+# Copyright (C) 2001 Jean-Christophe Filliâtre
 #   from a first script by Georges Mariano
 #
 # This library is free software; you can redistribute it and/or
@@ -78,12 +77,6 @@ AC_ARG_ENABLE(bench,
     [  --enable-bench          enable Why3 benchmarking tool],,
     enable_bench=yes)
 
-# dynlink
-
-AC_ARG_ENABLE(plugins,
-    [  --enable-plugins        enable Why3 plugins],,
-    enable_plugins=yes)
-
 # Coq plugin
 
 AC_ARG_ENABLE(coq-support,
@@ -152,12 +145,6 @@ case "$OCAMLVERSION" in
         AC_MSG_ERROR(You need Objective Caml 3.11.2 or higher);;
 esac
 
-if test "$enable_plugins" = "yes" ; then
-    DYNLINK="Dynlink"
-else
-    DYNLINK="Dynlink_"
-fi
-
 # Ocaml library path
 # old way: OCAMLLIB=`$OCAMLC -v | tail -1 | cut -f 4 -d ' ' | tr -d '\\r'`
 OCAMLLIB=`$OCAMLC -where | tr -d '\\r'`
@@ -433,13 +420,6 @@ else
    META_OCAMLGRAPH=""
 fi
 
-if test "$enable_plugins" = yes; then
-  META_DYNLINK="dynlink"
-else
-  META_DYNLINK=""
-fi
-
-
 #Viewer for ps and pdf
 dnl AC_CHECK_PROGS(PSVIEWER,gv evince)
 dnl AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince)
@@ -482,9 +462,6 @@ AC_SUBST(MENHIRLIB)
 AC_SUBST(LABLGTK2LIB)
 AC_SUBST(SQLITE3LIB)
 AC_SUBST(enable_bench)
-AC_SUBST(enable_plugins)
-AC_SUBST(DYNLINK)
-AC_SUBST(META_DYNLINK)
 AC_SUBST(META_OCAMLGRAPH)
 
 AC_SUBST(enable_coq_support)
@@ -532,7 +509,6 @@ echo "Verbose make            : $enable_verbose_make"
 echo "Why IDE                 : $enable_ide $reason_ide"
 echo "Why bench tool          : $enable_bench"
 echo "Why documentation       : $enable_doc"
-echo "Why plugins             : $enable_plugins"
 echo "Coq plugin support      : $enable_coq_support $reason_coq_support"
 if test "$enable_coq_support" = "yes" ; then
    echo "    Version             : $COQVERSION"

src/config.sh.in

@@ -5,7 +5,6 @@ config=src/config.ml
 libdir="$LIBDIR/why3"
 datadir="$DATADIR/why3"
 localdir="None"
-plugins="false"
 
 if [ "@enable_local@" = "yes" ]; then
     libdir="@LOCALDIR@/lib"
@@ -13,10 +12,6 @@ if [ "@enable_local@" = "yes" ]; then
     localdir="Some \"@LOCALDIR@\""
 fi
 
-if [ "@enable_plugins@" = "yes" ]; then
-    plugins="true"
-fi
-
 echo "
 let version   = \"@VERSION@\"
 let builddate = \"@BUILDDATE@\"
@@ -24,19 +19,4 @@ let builddate = \"@BUILDDATE@\"
 let libdir    = \"$libdir\"
 let datadir   = \"$datadir\"
 let localdir  = $localdir
-
-let plugins   = $plugins
-
-module Dynlink_ = struct
-  let is_native = true
-  let loadfile_private _ = assert false
-
-  type error
-  exception Error of error
-  let error_message _ = (assert false : string)
-end
-
-module Dynlink = struct
-  include @DYNLINK@
-end
 " > $config

src/driver/driver.ml

@@ -49,13 +49,10 @@ type driver = {
 
 (** parse a driver file *)
 
-exception NoPlugins
-
 let load_plugin dir (byte,nat) =
-  if not Config.plugins then raise NoPlugins;
-  let file = if Config.Dynlink.is_native then nat else byte in
+  let file = if Dynlink.is_native then nat else byte in
   let file = Filename.concat dir file in
-  Config.Dynlink.loadfile_private file
+  Dynlink.loadfile_private file
 
 let load_file file =
   let basename = Filename.dirname file in
@@ -321,8 +318,6 @@ let string_of_qualid thl idl =
 let () = Exn_printer.register (fun fmt exn -> match exn with
   | NoPrinter -> Format.fprintf fmt
       "No printer specified in the driver file"
-  | NoPlugins -> Format.fprintf fmt
-      "Plugins are not supported, recomplie Why3"
   | Duplicate s -> Format.fprintf fmt
       "Duplicate %s specification" s
   | UnknownType (thl,idl) -> Format.fprintf fmt

src/util/exn_printer.ml

@@ -43,11 +43,3 @@ let exn_printer fmt exn =
   try Stack.iter test exn_printers
   with Exit_loop -> ()
 
-(** For Config *)
-
-let () = register
-  (fun fmt exn -> match exn with
-    | Config.Dynlink.Error error ->
-        Format.fprintf fmt "Dynlink: %s" (Config.Dynlink.error_message error)
-    | _ -> raise exn)
-