support for user-defined Isabelle/Scala command-line tools;
authorwenzelm
Sat Nov 10 14:08:02 2018 +0100 (12 months ago)
changeset 69277258bef08b31e
parent 69276 3d954183b707
child 69278 30f6e8d2cd96
support for user-defined Isabelle/Scala command-line tools;
misc tuning and clarification;
NEWS
etc/settings
lib/scripts/getfunctions
src/Pure/Admin/build_cygwin.scala
src/Pure/Admin/build_doc.scala
src/Pure/Admin/build_jdk.scala
src/Pure/Admin/build_polyml.scala
src/Pure/Admin/build_status.scala
src/Pure/Admin/check_sources.scala
src/Pure/Admin/remote_dmg.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
src/Pure/Thy/file_format.scala
src/Tools/VSCode/src/build_vscode.scala
     1.1 --- a/NEWS	Sat Nov 10 07:57:20 2018 +0000
     1.2 +++ b/NEWS	Sat Nov 10 14:08:02 2018 +0100
     1.3 @@ -26,9 +26,9 @@
     1.4  OpenJDK 11.
     1.5  
     1.6  * Support for user-defined file-formats via class isabelle.File_Format
     1.7 -in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format). It is
     1.8 -configured via the shell function "isabelle_file_format" in
     1.9 -etc/settings, e.g. of an Isabelle component.
    1.10 +in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via
    1.11 +the shell function "isabelle_file_format" in etc/settings (e.g. of an
    1.12 +Isabelle component).
    1.13  
    1.14  
    1.15  *** Isar ***
    1.16 @@ -117,6 +117,11 @@
    1.17  
    1.18  *** System ***
    1.19  
    1.20 +* Support for Isabelle command-line tools defined in Isabelle/Scala.
    1.21 +Instances of class Isabelle_Scala_Tools may be configured via the shell
    1.22 +function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
    1.23 +component).
    1.24 +
    1.25  * Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
    1.26  source modules for Isabelle tools implemented in Haskell, notably for
    1.27  Isabelle/PIDE.
     2.1 --- a/etc/settings	Sat Nov 10 07:57:20 2018 +0000
     2.2 +++ b/etc/settings	Sat Nov 10 14:08:02 2018 +0100
     2.3 @@ -20,6 +20,9 @@
     2.4  
     2.5  classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
     2.6  
     2.7 +isabelle_scala_tools 'isabelle.Regular_Tools'
     2.8 +[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
     2.9 +
    2.10  isabelle_file_format 'isabelle.Bibtex$File_Format'
    2.11  
    2.12  #paranoia settings -- avoid intrusion of alien options
     3.1 --- a/lib/scripts/getfunctions	Sat Nov 10 07:57:20 2018 +0000
     3.2 +++ b/lib/scripts/getfunctions	Sat Nov 10 14:08:02 2018 +0100
     3.3 @@ -109,19 +109,35 @@
     3.4  }
     3.5  export -f classpath
     3.6  
     3.7 +#Isabelle/Scala tools
     3.8 +function isabelle_scala_tools ()
     3.9 +{
    3.10 +  local X=""
    3.11 +  for X in "$@"
    3.12 +  do
    3.13 +    if [ -z "$ISABELLE_SCALA_TOOLS" ]; then
    3.14 +      ISABELLE_SCALA_TOOLS="$X"
    3.15 +    else
    3.16 +      ISABELLE_SCALA_TOOLS="$ISABELLE_SCALA_TOOLS:$X"
    3.17 +    fi
    3.18 +  done
    3.19 +  export ISABELLE_SCALA_TOOLS
    3.20 +}
    3.21 +export -f isabelle_scala_tools
    3.22 +
    3.23  #file formats
    3.24  function isabelle_file_format ()
    3.25  {
    3.26    local X=""
    3.27    for X in "$@"
    3.28    do
    3.29 -    if [ -z "$ISABELLE_CLASSES_FILE_FORMAT" ]; then
    3.30 -      ISABELLE_CLASSES_FILE_FORMAT="$X"
    3.31 +    if [ -z "$ISABELLE_FILE_FORMATS" ]; then
    3.32 +      ISABELLE_FILE_FORMATS="$X"
    3.33      else
    3.34 -      ISABELLE_CLASSES_FILE_FORMAT="$ISABELLE_CLASSES_FILE_FORMAT:$X"
    3.35 +      ISABELLE_FILE_FORMATS="$ISABELLE_FILE_FORMATS:$X"
    3.36      fi
    3.37    done
    3.38 -  export ISABELLE_CLASSES_FILE_FORMAT
    3.39 +  export ISABELLE_FILE_FORMATS
    3.40  }
    3.41  export -f isabelle_file_format
    3.42  
     4.1 --- a/src/Pure/Admin/build_cygwin.scala	Sat Nov 10 07:57:20 2018 +0000
     4.2 +++ b/src/Pure/Admin/build_cygwin.scala	Sat Nov 10 14:08:02 2018 +0100
     4.3 @@ -87,5 +87,5 @@
     4.4        if (more_args.nonEmpty) getopts.usage()
     4.5  
     4.6        build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
     4.7 -    }, admin = true)
     4.8 +    })
     4.9  }
     5.1 --- a/src/Pure/Admin/build_doc.scala	Sat Nov 10 07:57:20 2018 +0000
     5.2 +++ b/src/Pure/Admin/build_doc.scala	Sat Nov 10 14:08:02 2018 +0100
     5.3 @@ -105,5 +105,5 @@
     5.4            build_doc(options, progress, all_docs, max_jobs, system_mode, docs)
     5.5          }
     5.6        sys.exit(rc)
     5.7 -    }, admin = true)
     5.8 +    })
     5.9  }
     6.1 --- a/src/Pure/Admin/build_jdk.scala	Sat Nov 10 07:57:20 2018 +0000
     6.2 +++ b/src/Pure/Admin/build_jdk.scala	Sat Nov 10 14:08:02 2018 +0100
     6.3 @@ -237,5 +237,5 @@
     6.4        val progress = new Console_Progress()
     6.5  
     6.6        build_jdk(archives = archives, progress = progress, target_dir = target_dir)
     6.7 -    }, admin = true)
     6.8 +    })
     6.9  }
     7.1 --- a/src/Pure/Admin/build_polyml.scala	Sat Nov 10 07:57:20 2018 +0000
     7.2 +++ b/src/Pure/Admin/build_polyml.scala	Sat Nov 10 14:08:02 2018 +0100
     7.3 @@ -272,7 +272,7 @@
     7.4          build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress,
     7.5            arch_64 = arch_64, options = options, msys_root = msys_root)
     7.6        }
     7.7 -    }, admin = true)
     7.8 +    })
     7.9  
    7.10    val isabelle_tool2 =
    7.11      Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", args =>
    7.12 @@ -298,5 +298,5 @@
    7.13            }
    7.14          build_polyml_component(component, sha1_root = sha1_root)
    7.15        }
    7.16 -    }, admin = true)
    7.17 +    })
    7.18  }
     8.1 --- a/src/Pure/Admin/build_status.scala	Sat Nov 10 07:57:20 2018 +0000
     8.2 +++ b/src/Pure/Admin/build_status.scala	Sat Nov 10 14:08:02 2018 +0100
     8.3 @@ -591,6 +591,5 @@
     8.4  
     8.5        build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
     8.6          target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
     8.7 -
     8.8 -  }, admin = true)
     8.9 +    })
    8.10  }
     9.1 --- a/src/Pure/Admin/check_sources.scala	Sat Nov 10 07:57:20 2018 +0000
     9.2 +++ b/src/Pure/Admin/check_sources.scala	Sat Nov 10 14:08:02 2018 +0100
     9.3 @@ -70,5 +70,5 @@
     9.4        if (specs.isEmpty) getopts.usage()
     9.5  
     9.6        for (root <- specs) check_hg(Path.explode(root))
     9.7 -    }, admin = true)
     9.8 +    })
     9.9  }
    10.1 --- a/src/Pure/Admin/remote_dmg.scala	Sat Nov 10 07:57:20 2018 +0000
    10.2 +++ b/src/Pure/Admin/remote_dmg.scala	Sat Nov 10 14:08:02 2018 +0100
    10.3 @@ -60,5 +60,5 @@
    10.4          using(SSH.open_session(options, host = host, user = user, port = port))(
    10.5            remote_dmg(_, tar_gz_file, dmg_file, volume_name))
    10.6        }
    10.7 -    }, admin = true)
    10.8 +    })
    10.9  }
    11.1 --- a/src/Pure/System/isabelle_system.scala	Sat Nov 10 07:57:20 2018 +0000
    11.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Nov 10 14:08:02 2018 +0100
    11.3 @@ -347,6 +347,24 @@
    11.4      Path.split(getenv_strict("ISABELLE_COMPONENTS"))
    11.5  
    11.6  
    11.7 +  /* classes */
    11.8 +
    11.9 +  def init_classes[A](variable: String): List[A] =
   11.10 +  {
   11.11 +    for (name <- space_explode(':', Isabelle_System.getenv_strict(variable)))
   11.12 +    yield {
   11.13 +      def err(msg: String): Nothing =
   11.14 +        error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
   11.15 +
   11.16 +      try { Class.forName(name).asInstanceOf[Class[A]].newInstance() }
   11.17 +      catch {
   11.18 +        case _: ClassNotFoundException => err("Class not found")
   11.19 +        case exn: Throwable => err(Exn.message(exn))
   11.20 +      }
   11.21 +    }
   11.22 +  }
   11.23 +
   11.24 +
   11.25    /* fonts */
   11.26  
   11.27    def fonts(html: Boolean = false, get: String => String = getenv_strict(_)): List[Path] =
    12.1 --- a/src/Pure/System/isabelle_tool.scala	Sat Nov 10 07:57:20 2018 +0000
    12.2 +++ b/src/Pure/System/isabelle_tool.scala	Sat Nov 10 14:08:02 2018 +0100
    12.3 @@ -97,44 +97,17 @@
    12.4  
    12.5    /* internal tools */
    12.6  
    12.7 -  private val internal_tools: List[Isabelle_Tool] =
    12.8 -    List(
    12.9 -      Build.isabelle_tool,
   12.10 -      Build_Cygwin.isabelle_tool,
   12.11 -      Build_Doc.isabelle_tool,
   12.12 -      Build_Docker.isabelle_tool,
   12.13 -      Build_JDK.isabelle_tool,
   12.14 -      Build_PolyML.isabelle_tool1,
   12.15 -      Build_PolyML.isabelle_tool2,
   12.16 -      Build_Status.isabelle_tool,
   12.17 -      Check_Sources.isabelle_tool,
   12.18 -      Doc.isabelle_tool,
   12.19 -      Dump.isabelle_tool,
   12.20 -      Export.isabelle_tool,
   12.21 -      Imports.isabelle_tool,
   12.22 -      Mkroot.isabelle_tool,
   12.23 -      ML_Process.isabelle_tool,
   12.24 -      Options.isabelle_tool,
   12.25 -      Present.isabelle_tool,
   12.26 -      Profiling_Report.isabelle_tool,
   12.27 -      Remote_DMG.isabelle_tool,
   12.28 -      Server.isabelle_tool,
   12.29 -      Update_Cartouches.isabelle_tool,
   12.30 -      Update_Comments.isabelle_tool,
   12.31 -      Update_Header.isabelle_tool,
   12.32 -      Update_Then.isabelle_tool,
   12.33 -      Update_Theorems.isabelle_tool,
   12.34 -      isabelle.vscode.Build_VSCode.isabelle_tool,
   12.35 -      isabelle.vscode.Grammar.isabelle_tool,
   12.36 -      isabelle.vscode.Server.isabelle_tool)
   12.37 +  private lazy val internal_tools: List[Isabelle_Tool] =
   12.38 +    Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
   12.39 +      .flatMap(_.tools.toList)
   12.40  
   12.41    private def list_internal(): List[(String, String)] =
   12.42 -    for (tool <- internal_tools.toList if tool.accessible)
   12.43 +    for (tool <- internal_tools.toList)
   12.44        yield (tool.name, tool.description)
   12.45  
   12.46    private def find_internal(name: String): Option[List[String] => Unit] =
   12.47      internal_tools.collectFirst({
   12.48 -      case tool if tool.name == name && tool.accessible =>
   12.49 +      case tool if tool.name == name =>
   12.50          args => Command_Line.tool0 { tool.body(args) }
   12.51        })
   12.52  
   12.53 @@ -165,8 +138,38 @@
   12.54    }
   12.55  }
   12.56  
   12.57 -sealed case class Isabelle_Tool(
   12.58 -  name: String, description: String, body: List[String] => Unit, admin: Boolean = false)
   12.59 -{
   12.60 -  def accessible: Boolean = !admin || Isabelle_System.admin()
   12.61 -}
   12.62 +sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
   12.63 +
   12.64 +class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
   12.65 +
   12.66 +class Regular_Tools extends Isabelle_Scala_Tools(
   12.67 +  Build.isabelle_tool,
   12.68 +  Build_Docker.isabelle_tool,
   12.69 +  Doc.isabelle_tool,
   12.70 +  Dump.isabelle_tool,
   12.71 +  Export.isabelle_tool,
   12.72 +  Imports.isabelle_tool,
   12.73 +  ML_Process.isabelle_tool,
   12.74 +  Mkroot.isabelle_tool,
   12.75 +  Options.isabelle_tool,
   12.76 +  Present.isabelle_tool,
   12.77 +  Profiling_Report.isabelle_tool,
   12.78 +  Server.isabelle_tool,
   12.79 +  Update_Cartouches.isabelle_tool,
   12.80 +  Update_Comments.isabelle_tool,
   12.81 +  Update_Header.isabelle_tool,
   12.82 +  Update_Then.isabelle_tool,
   12.83 +  Update_Theorems.isabelle_tool,
   12.84 +  isabelle.vscode.Grammar.isabelle_tool,
   12.85 +  isabelle.vscode.Server.isabelle_tool)
   12.86 +
   12.87 +class Admin_Tools extends Isabelle_Scala_Tools(
   12.88 +  Build_Cygwin.isabelle_tool,
   12.89 +  Build_Doc.isabelle_tool,
   12.90 +  Build_JDK.isabelle_tool,
   12.91 +  Build_PolyML.isabelle_tool1,
   12.92 +  Build_PolyML.isabelle_tool2,
   12.93 +  Build_Status.isabelle_tool,
   12.94 +  Check_Sources.isabelle_tool,
   12.95 +  Remote_DMG.isabelle_tool,
   12.96 +  isabelle.vscode.Build_VSCode.isabelle_tool)
    13.1 --- a/src/Pure/Thy/file_format.scala	Sat Nov 10 07:57:20 2018 +0000
    13.2 +++ b/src/Pure/Thy/file_format.scala	Sat Nov 10 14:08:02 2018 +0100
    13.3 @@ -10,21 +10,7 @@
    13.4  object File_Format
    13.5  {
    13.6    def environment(): Environment =
    13.7 -  {
    13.8 -    val file_formats =
    13.9 -      for (name <- space_explode(':', Isabelle_System.getenv_strict("ISABELLE_CLASSES_FILE_FORMAT")))
   13.10 -      yield {
   13.11 -        def err(msg: String): Nothing =
   13.12 -          error("Bad entry " + quote(name) + " in ISABELLE_CLASSES_FILE_FORMAT\n" + msg)
   13.13 -
   13.14 -        try { Class.forName(name).asInstanceOf[Class[File_Format]].newInstance() }
   13.15 -        catch {
   13.16 -          case _: ClassNotFoundException => err("Class not found")
   13.17 -          case exn: Throwable => err(Exn.message(exn))
   13.18 -        }
   13.19 -      }
   13.20 -    new Environment(file_formats)
   13.21 -  }
   13.22 +    new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
   13.23  
   13.24    final class Environment private [File_Format](file_formats: List[File_Format])
   13.25    {
    14.1 --- a/src/Tools/VSCode/src/build_vscode.scala	Sat Nov 10 07:57:20 2018 +0000
    14.2 +++ b/src/Tools/VSCode/src/build_vscode.scala	Sat Nov 10 14:08:02 2018 +0100
    14.3 @@ -70,5 +70,5 @@
    14.4  
    14.5        build_grammar(options, progress)
    14.6        build_extension(progress, publish = publish)
    14.7 -    }, admin = true)
    14.8 +    })
    14.9  }