merged
authorwenzelm
Thu Jun 25 13:36:46 2009 +0200 (2009-06-25 ago)
changeset 31801b97b34e7c853
parent 31800 477f2abf90a4
parent 31797 203d5e61e3bc
child 31802 a36b5e02c1ab
merged
     1.1 --- a/bin/isabelle-process	Thu Jun 25 13:00:32 2009 +0200
     1.2 +++ b/bin/isabelle-process	Thu Jun 25 13:36:46 2009 +0200
     1.3 @@ -214,7 +214,7 @@
     1.4  NICE="nice"
     1.5  if [ -n "$WRAPPER_OUTPUT" ]; then
     1.6    [ "$WRAPPER_OUTPUT" = "-" -o -p "$WRAPPER_OUTPUT" ] || fail "Bad named pipe: $WRAPPER_OUTPUT"
     1.7 -  MLTEXT="$MLTEXT; IsabelleProcess.init \"$WRAPPER_OUTPUT\";"
     1.8 +  MLTEXT="$MLTEXT; Isabelle_Process.init \"$WRAPPER_OUTPUT\";"
     1.9  elif [ -n "$PGIP" ]; then
    1.10    MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
    1.11  elif [ -n "$PROOFGENERAL" ]; then
     2.1 --- a/src/Pure/Isar/isar.scala	Thu Jun 25 13:00:32 2009 +0200
     2.2 +++ b/src/Pure/Isar/isar.scala	Thu Jun 25 13:36:46 2009 +0200
     2.3 @@ -7,8 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 -class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
     2.8 -  extends IsabelleProcess(isabelle_system, results, args: _*)
     2.9 +class Isar(isabelle_system: Isabelle_System,
    2.10 +    results: EventBus[Isabelle_Process.Result], args: String*)
    2.11 +  extends Isabelle_Process(isabelle_system, results, args: _*)
    2.12  {
    2.13    /* basic editor commands */
    2.14  
     3.1 --- a/src/Pure/Isar/isar_document.scala	Thu Jun 25 13:00:32 2009 +0200
     3.2 +++ b/src/Pure/Isar/isar_document.scala	Thu Jun 25 13:36:46 2009 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    type Document_ID = String
     3.5  }
     3.6  
     3.7 -trait IsarDocument extends IsabelleProcess
     3.8 +trait IsarDocument extends Isabelle_Process
     3.9  {
    3.10    import IsarDocument._
    3.11  
     4.1 --- a/src/Pure/System/isabelle_process.ML	Thu Jun 25 13:00:32 2009 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Jun 25 13:36:46 2009 +0200
     4.3 @@ -27,7 +27,7 @@
     4.4    val init: string -> unit
     4.5  end;
     4.6  
     4.7 -structure IsabelleProcess: ISABELLE_PROCESS =
     4.8 +structure Isabelle_Process: ISABELLE_PROCESS =
     4.9  struct
    4.10  
    4.11  (* print modes *)
     5.1 --- a/src/Pure/System/isabelle_process.scala	Thu Jun 25 13:00:32 2009 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Jun 25 13:36:46 2009 +0200
     5.3 @@ -12,7 +12,7 @@
     5.4    InputStream, OutputStream, IOException}
     5.5  
     5.6  
     5.7 -object IsabelleProcess {
     5.8 +object Isabelle_Process {
     5.9  
    5.10    /* results */
    5.11  
    5.12 @@ -96,7 +96,7 @@
    5.13      def is_system = Kind.is_system(kind)
    5.14    }
    5.15  
    5.16 -  def parse_message(isabelle_system: IsabelleSystem, result: Result) =
    5.17 +  def parse_message(isabelle_system: Isabelle_System, result: Result) =
    5.18    {
    5.19      XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
    5.20        YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
    5.21 @@ -104,16 +104,16 @@
    5.22  }
    5.23  
    5.24  
    5.25 -class IsabelleProcess(isabelle_system: IsabelleSystem,
    5.26 -  results: EventBus[IsabelleProcess.Result], args: String*)
    5.27 +class Isabelle_Process(isabelle_system: Isabelle_System,
    5.28 +  results: EventBus[Isabelle_Process.Result], args: String*)
    5.29  {
    5.30 -  import IsabelleProcess._
    5.31 +  import Isabelle_Process._
    5.32  
    5.33  
    5.34    /* demo constructor */
    5.35  
    5.36    def this(args: String*) =
    5.37 -    this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
    5.38 +    this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*)
    5.39  
    5.40  
    5.41    /* process information */
    5.42 @@ -128,7 +128,7 @@
    5.43    /* results */
    5.44  
    5.45    def parse_message(result: Result): XML.Tree =
    5.46 -    IsabelleProcess.parse_message(isabelle_system, result)
    5.47 +    Isabelle_Process.parse_message(isabelle_system, result)
    5.48  
    5.49    private val result_queue = new LinkedBlockingQueue[Result]
    5.50  
    5.51 @@ -230,7 +230,7 @@
    5.52  
    5.53    private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
    5.54      override def run() = {
    5.55 -      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
    5.56 +      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Isabelle_System.charset))
    5.57        var finished = false
    5.58        while (!finished) {
    5.59          try {
    5.60 @@ -260,7 +260,7 @@
    5.61  
    5.62    private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
    5.63      override def run() = {
    5.64 -      val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
    5.65 +      val reader = new BufferedReader(new InputStreamReader(in_stream, Isabelle_System.charset))
    5.66        var result = new StringBuilder(100)
    5.67  
    5.68        var finished = false
     6.1 --- a/src/Pure/System/isabelle_system.scala	Thu Jun 25 13:00:32 2009 +0200
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jun 25 13:36:46 2009 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  /*  Title:      Pure/System/isabelle_system.scala
     6.5      Author:     Makarius
     6.6  
     6.7 -Isabelle system support -- basic Cygwin/Posix compatibility.
     6.8 +Isabelle system support, with basic Cygwin/Posix compatibility.
     6.9  */
    6.10  
    6.11  package isabelle
    6.12 @@ -13,7 +13,7 @@
    6.13  import scala.util.matching.Regex
    6.14  
    6.15  
    6.16 -object IsabelleSystem
    6.17 +object Isabelle_System
    6.18  {
    6.19  
    6.20    val charset = "UTF-8"
    6.21 @@ -48,20 +48,23 @@
    6.22  }
    6.23  
    6.24  
    6.25 -class IsabelleSystem
    6.26 +class Isabelle_System
    6.27  {
    6.28  
    6.29 -  /* unique ids */
    6.30 +  /** unique ids **/
    6.31  
    6.32    private var id_count: BigInt = 0
    6.33    def id(): String = synchronized { id_count += 1; "j" + id_count }
    6.34  
    6.35  
    6.36 -  /* Isabelle settings environment */
    6.37 +
    6.38 +  /** Isabelle environment **/
    6.39 +
    6.40 +  /* platform prefixes */
    6.41  
    6.42    private val (platform_root, drive_prefix, shell_prefix) =
    6.43    {
    6.44 -    if (IsabelleSystem.is_cygwin) {
    6.45 +    if (Isabelle_System.is_cygwin) {
    6.46        val root = Cygwin.root() getOrElse "C:\\cygwin"
    6.47        val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
    6.48        val shell = List(root + "\\bin\\bash", "-l")
    6.49 @@ -70,6 +73,9 @@
    6.50      else ("/", "", Nil)
    6.51    }
    6.52  
    6.53 +
    6.54 +  /* bash environment */
    6.55 +
    6.56    private val environment: Map[String, String] =
    6.57    {
    6.58      import scala.collection.jcl.Conversions._
    6.59 @@ -88,8 +94,8 @@
    6.60      val dump = File.createTempFile("isabelle", null)
    6.61      try {
    6.62        val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
    6.63 -      val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*)
    6.64 -      val (output, rc) = IsabelleSystem.process_output(proc)
    6.65 +      val proc = Isabelle_System.raw_execute(env0, true, cmdline: _*)
    6.66 +      val (output, rc) = Isabelle_System.process_output(proc)
    6.67        if (rc != 0) error(output)
    6.68  
    6.69        val entries =
    6.70 @@ -105,10 +111,11 @@
    6.71      finally { dump.delete }
    6.72    }
    6.73  
    6.74 +
    6.75 +  /* getenv */
    6.76 +
    6.77    def getenv(name: String): String =
    6.78 -  {
    6.79      environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
    6.80 -  }
    6.81  
    6.82    def getenv_strict(name: String): String =
    6.83    {
    6.84 @@ -119,7 +126,43 @@
    6.85    override def toString = getenv("ISABELLE_HOME")
    6.86  
    6.87  
    6.88 -  /* file path specifications */
    6.89 +
    6.90 +  /** file path specifications **/
    6.91 +
    6.92 +  /* Isabelle paths */
    6.93 +
    6.94 +  def expand_path(source_path: String): String =
    6.95 +  {
    6.96 +    val result_path = new StringBuilder
    6.97 +    def init(path: String)
    6.98 +    {
    6.99 +      if (path.startsWith("/")) {
   6.100 +        result_path.clear
   6.101 +        result_path += '/'
   6.102 +      }
   6.103 +    }
   6.104 +    def append(path: String)
   6.105 +    {
   6.106 +      init(path)
   6.107 +      for (p <- path.split("/") if p != "") {
   6.108 +        val len = result_path.length
   6.109 +        if (len > 0 && result_path(len - 1) != '/')
   6.110 +          result_path += '/'
   6.111 +        result_path ++= p
   6.112 +      }
   6.113 +    }
   6.114 +    init(source_path)
   6.115 +    for (p <- source_path.split("/")) {
   6.116 +      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
   6.117 +      else if (p == "~") append(getenv_strict("HOME"))
   6.118 +      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
   6.119 +      else append(p)
   6.120 +    }
   6.121 +    result_path.toString
   6.122 +  }
   6.123 +
   6.124 +
   6.125 +  /* platform paths */
   6.126  
   6.127    private val Cygdrive = new Regex(
   6.128      if (drive_prefix == "") "\0"
   6.129 @@ -128,39 +171,21 @@
   6.130    def platform_path(source_path: String): String =
   6.131    {
   6.132      val result_path = new StringBuilder
   6.133 -
   6.134 -    def init(path: String): String =
   6.135 -    {
   6.136 -      path match {
   6.137 +    val rest =
   6.138 +      expand_path(source_path) match {
   6.139          case Cygdrive(drive, rest) =>
   6.140 -          result_path.length = 0
   6.141 -          result_path.append(drive)
   6.142 -          result_path.append(":")
   6.143 -          result_path.append(File.separator)
   6.144 +          result_path ++= (drive + ":" + File.separator)
   6.145            rest
   6.146 -        case _ if (path.startsWith("/")) =>
   6.147 -          result_path.length = 0
   6.148 -          result_path.append(platform_root)
   6.149 -          path.substring(1)
   6.150 -        case _ => path
   6.151 +        case path if path.startsWith("/") =>
   6.152 +          result_path ++= platform_root
   6.153 +          path
   6.154 +        case path => path
   6.155        }
   6.156 -    }
   6.157 -    def append(path: String)
   6.158 -    {
   6.159 -      for (p <- init(path) split "/") {
   6.160 -        if (p != "") {
   6.161 -          val len = result_path.length
   6.162 -          if (len > 0 && result_path(len - 1) != File.separatorChar)
   6.163 -            result_path.append(File.separator)
   6.164 -          result_path.append(p)
   6.165 -        }
   6.166 -      }
   6.167 -    }
   6.168 -    for (p <- init(source_path) split "/") {
   6.169 -      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
   6.170 -      else if (p == "~") append(getenv_strict("HOME"))
   6.171 -      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
   6.172 -      else append(p)
   6.173 +    for (p <- rest.split("/") if p != "") {
   6.174 +      val len = result_path.length
   6.175 +      if (len > 0 && result_path(len - 1) != File.separatorChar)
   6.176 +        result_path += File.separatorChar
   6.177 +      result_path ++= p
   6.178      }
   6.179      result_path.toString
   6.180    }
   6.181 @@ -186,20 +211,22 @@
   6.182    }
   6.183  
   6.184  
   6.185 +  /** system tools **/
   6.186 +
   6.187    /* external processes */
   6.188  
   6.189    def execute(redirect: Boolean, args: String*): Process =
   6.190    {
   6.191      val cmdline =
   6.192 -      if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args
   6.193 +      if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args
   6.194        else args
   6.195 -    IsabelleSystem.raw_execute(environment, redirect, cmdline: _*)
   6.196 +    Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
   6.197    }
   6.198  
   6.199    def isabelle_tool(args: String*): (String, Int) =
   6.200    {
   6.201      val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
   6.202 -    IsabelleSystem.process_output(proc)
   6.203 +    Isabelle_System.process_output(proc)
   6.204    }
   6.205  
   6.206  
   6.207 @@ -222,12 +249,14 @@
   6.208    {
   6.209      // blocks until writer is ready
   6.210      val stream =
   6.211 -      if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream
   6.212 +      if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream
   6.213        else new FileInputStream(fifo)
   6.214 -    new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset))
   6.215 +    new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
   6.216    }
   6.217  
   6.218  
   6.219 +  /** Isabelle resources **/
   6.220 +
   6.221    /* find logics */
   6.222  
   6.223    def find_logics(): List[String] =